aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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.
* 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.
| * 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
| |
* | 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
| | * | use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
| |/ / |/| |
* | | Update CHANGESGravatar Matthieu Sozeau2017-12-01
| |/ |/|
* | Merge PR #6276: Coqchk accepts filenamesGravatar Maxime Dénès2017-12-01
|\ \
* | | Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
| * | Documenting the possibility to pass filenames to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
|/ /
| * Selecting which notation to print based on current stack of scope.Gravatar Hugo Herbelin2017-11-27
|/ | | | | | See discussion on coq-club starting on 23 August 2016. An open question: what priority to give to "abbreviations"?
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
* Moving bug numbers to BZ# format in the CHANGES file.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (ba7fa6b in #960), this commit only re-formats bug numbers that are also PR numbers.
* Merge PR #540: [configure] Support for flambda flags.Gravatar Maxime Dénès2017-10-10
|\
* \ Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\ \
| | * [configure] Support for flambda flags.Gravatar Emilio Jesus Gallego Arias2017-10-10
| |/ |/| | | | | | | | | | | | | | | We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ```
* | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵Gravatar Maxime Dénès2017-10-09
|\ \ | | | | | | | | | printing-ony Notations
* | | 8.7+beta2 CHANGESGravatar Théo Zimmermann2017-10-06
| | |
| | * romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When a context variable x is of the form "x := body : Z", romega is now made aware of this body. Technically, we reify an equation x = body, and push a corresponding (eq_refl x) as argument of the final do_omega. See also the previous commit adding this same feature to omega (fixing bug 142).
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 09:35:15 +0000