aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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.
| * / / 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
|\
* \ Merge PR #6381: A version of [time] that works on constr evaluationGravatar Maxime Dénès2017-12-18
|\ \
* \ \ Merge PR #6380: Add tactics to reset and display the Ltac profileGravatar Maxime Dénès2017-12-18
|\ \ \
* \ \ \ Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵Gravatar Maxime Dénès2017-12-18
|\ \ \ \ | | | | | | | | | | | | | | | Extraction Language command
| | | | * Removing the FAQ, which has been moved to the GitHub wiki for thisGravatar Matt Quinn2017-12-18
| | | | | | | | | | | | | | | | | | | | repository. Also removing FAQ-related build rules.
* | | | | Merge PR #6429: 8.7.1 CHANGES.Gravatar Maxime Dénès2017-12-15
|\ \ \ \ \
| | | | * | Add documentation for time_constrGravatar Jason Gross2017-12-14
| | | |/ /
| | | * / Add doc+changelog entries for new LtacProf tacticsGravatar Jason Gross2017-12-14
| |_|/ / |/| | |
| * | | 8.7.1 CHANGES.Gravatar Théo Zimmermann2017-12-14
| | | |
* | | | In printing, factorizing "match" clauses with same right-hand side.Gravatar Hugo Herbelin2017-12-12
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Moreover, when there are at least two clauses and the last most factorizable one is a disjunction with no variables, turn it into a catch-all clause. Adding options Unset Printing Allow Default Clause. to deactivate the second behavior, and Unset Printing Factorizable Match Patterns. to deactivate the first behavior (deactivating the first one deactivates also the second one). E.g. printing match x with Eq => 1 | _ => 0 end gives match x with | Eq => 1 | _ => 0 end or (with default clause deactivates): match x with | Eq => 1 | Lt | Gt => 0 end More to be done, e.g. reconstructing multiple patterns in Nat.eqb...
* | | Merge PR #873: New strategy based on open scopes for deciding which notation ↵Gravatar Maxime Dénès2017-12-07
|\ \ \ | | | | | | | | | | | | to use among several of them
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 16:25:29 +0000