aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
...
* Merge PR #6949: Revert PR #873: New strategy based on open scopes for ↵Gravatar Maxime Dénès2018-03-09
|\ | | | | | | deciding…
* \ Merge PR #6775: Allow using cumulativity without forcing strict constraints.Gravatar Maxime Dénès2018-03-09
|\ \
| | * Revert "Merge PR #873: New strategy based on open scopes for deciding which ↵Gravatar Maxime Dénès2018-03-09
| | | | | | | | | | | | | | | | | | | | | notation to use among several of them" This reverts commit 9cac9db6446b31294d2413d920db0eaa6dd5d8a6, reversing changes made to 2f679ec5235257c9fd106c26c15049e04523a307.
* | | Merge PR #6923: Export optionsGravatar Maxime Dénès2018-03-09
|\ \ \ | |_|/ |/| |
| | * Documentation for Cumulativity Weak Constraints.Gravatar Gaëtan Gilbert2018-03-09
| | |
* | | Merge PR #6480: Allow Prop as source for coercionsGravatar Maxime Dénès2018-03-09
|\ \ \ | |_|/ |/| |
* | | Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\ \ \
| | | * Documenting the Export modifier for options in CHANGES.Gravatar Pierre-Marie Pédrot2018-03-09
| |_|/ |/| |
| | * doc and changes for coercion from prop/typeGravatar charguer2018-03-09
| |/ |/|
* | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵Gravatar Maxime Dénès2018-03-09
|\ \ | | | | | | | | | fiat-crypto/OSX
* \ \ Merge PR #6926: An experimental 'Show Extraction' command (grant feature ↵Gravatar Maxime Dénès2018-03-08
|\ \ \ | | | | | | | | | | | | wish #4129)
* \ \ \ Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6582: Mangle auto-generated namesGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* | | | | | | [vernac] Warn when using “Require” in a sectionGravatar Vincent Laporte2018-03-07
| | | | | | |
* | | | | | | Merge PR #6744: Add String.concatGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \ \
| | | | | | * | Add CHANGES and man entry for coqdep learning _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | |
| | | | | * | | An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| | | | | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Attempt to extract the current ongoing proof (request by Clément Pit-Claudel on coqdev, and also #4129). Evars are handled as axioms.
* | | | | | | CHANGES and tests for with Definition @{univs}Gravatar Gaëtan Gilbert2018-03-05
| | | | | | |
| | | * | | | Deprecate Focus and Unfocus.Gravatar Théo Zimmermann2018-03-05
| | | | |/ / | | | |/| |
* | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
| * | | | | | CHANGES entry for #6791.Gravatar Théo Zimmermann2018-03-02
| | |_|/ / / | |/| | | |
* / | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
|/ / / / / | | | | | | | | | | | | | | | Noticed by Sigurd Schneider.
| | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
| | | | |
| * | | | Add String.concatGravatar Jason Gross2018-02-24
|/ / / /
* | | | Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR #6604: Extend `zify_N` with knowledge about `N.pred`Gravatar Maxime Dénès2018-02-21
|\ \ \ \
| | * | | Add CHANGES entry for decimals in preludeGravatar Jason Gross2018-02-20
| | | | |
* | | | | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
* | | | | More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We generalize the possibility to refer to a notation not only by its "_ U _" form but also using its "a 'U' b". (Wish from EJGA)
* | | | | A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
| | | | |
* | | | | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
| | * | Implement name mangling optionGravatar Jasper Hugunin2018-02-17
| |/ / |/| |
| * | Extend `zify_N` with knowledge about `N.pred`Gravatar Joachim Breitner2018-02-14
| | | | | | | | | | | | | | | by doing the same thing as `zify_nat` does for `nat.pred`. This fixes #6602.
* | | CHANGES for 8.7.2.Gravatar Théo Zimmermann2018-02-14
|/ /
* | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Gravatar Maxime Dénès2018-02-14
|\ \
| * | Add CHANGES entry for #1047Gravatar Tej Chajed2018-02-13
| | |
| | * Add notation {x & P} for sigTGravatar Tej Chajed2018-02-12
| |/ | | | | | | | | Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified.
* / CHANGES for universe varianceGravatar Gaëtan Gilbert2018-02-12
|/
* Merge PR #6629: Archive COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\
| * Move the mention of the removal of Qed exporting at the right place.Gravatar Théo Zimmermann2018-01-22
| |
* | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \
* | | add flash infos about wrap, not found, no. of replacements, no. of finds, ↵Gravatar Paul Steckler2018-01-18
| |/ |/| | | | | issue #6452
* | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \
| | * Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| | |
| * | Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| |/
* | Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ | |/ |/|
| * Documentation and CHANGES for bracket with goal selector.Gravatar Théo Zimmermann2018-01-05
| |
* | add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
|/
* Merge PR #6377: Removal of the FAQ LaTex document.Gravatar Maxime Dénès2017-12-20
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 11:11:50 +0000