Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | CHANGES for 8.7.2. | 2018-02-14 | |
| | |||
* | Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation) | 2018-02-14 | |
|\ | |||
| * | Add CHANGES entry for #1047 | 2018-02-13 | |
| | | |||
* | | CHANGES for universe variance | 2018-02-12 | |
|/ | |||
* | Merge PR #6629: Archive COMPATIBILITY | 2018-01-23 | |
|\ | |||
| * | Move the mention of the removal of Qed exporting at the right place. | 2018-01-22 | |
| | | |||
* | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | 2018-01-22 | |
|\ \ | |||
* | | | add flash infos about wrap, not found, no. of replacements, no. of finds, ↵ | 2018-01-18 | |
| |/ |/| | | | | | issue #6452 | ||
* | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | 2018-01-18 | |
|\ \ | |||
| | * | Add CHANGES entry | 2018-01-17 | |
| | | | |||
| * | | Add CHANGES entry | 2018-01-17 | |
| |/ | |||
* | | Merge PR #6551: Bracket with goal selector | 2018-01-16 | |
|\ \ | |/ |/| | |||
| * | Documentation and CHANGES for bracket with goal selector. | 2018-01-05 | |
| | | |||
* | | add optimize_heap tactic for #6488 | 2018-01-03 | |
|/ | |||
* | Merge PR #6377: Removal of the FAQ LaTex document. | 2017-12-20 | |
|\ | |||
* \ | Merge PR #6381: A version of [time] that works on constr evaluation | 2017-12-18 | |
|\ \ | |||
* \ \ | Merge PR #6380: Add tactics to reset and display the Ltac profile | 2017-12-18 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | 2017-12-18 | |
|\ \ \ \ | | | | | | | | | | | | | | | | Extraction Language command | ||
| | | | * | Removing the FAQ, which has been moved to the GitHub wiki for this | 2017-12-18 | |
| | | | | | | | | | | | | | | | | | | | | repository. Also removing FAQ-related build rules. | ||
* | | | | | Merge PR #6429: 8.7.1 CHANGES. | 2017-12-15 | |
|\ \ \ \ \ | |||
| | | | * | | Add documentation for time_constr | 2017-12-14 | |
| | | |/ / | |||
| | | * / | Add doc+changelog entries for new LtacProf tactics | 2017-12-14 | |
| |_|/ / |/| | | | |||
| * | | | 8.7.1 CHANGES. | 2017-12-14 | |
| | | | | |||
* | | | | In printing, factorizing "match" clauses with same right-hand side. | 2017-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 ↵ | 2017-12-07 | |
|\ \ \ | | | | | | | | | | | | | to use among several of them | ||
| | * | | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | 2017-12-05 | |
| |/ / |/| | | |||
* | | | Update CHANGES | 2017-12-01 | |
| |/ |/| | |||
* | | Merge PR #6276: Coqchk accepts filenames | 2017-12-01 | |
|\ \ | |||
* | | | Remove "obsolete_locality" and fix STM vernac classification. | 2017-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. | 2017-11-29 | |
|/ / | |||
| * | Selecting which notation to print based on current stack of scope. | 2017-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 at | 2017-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. | 2017-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. | 2017-10-10 | |
|\ | |||
* \ | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | 2017-10-10 | |
|\ \ | |||
| | * | [configure] Support for flambda flags. | 2017-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 ↵ | 2017-10-09 | |
|\ \ | | | | | | | | | | printing-ony Notations | ||
* | | | 8.7+beta2 CHANGES | 2017-10-06 | |
| | | | |||
| | * | romega: takes advantage of context variables with body | 2017-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). | ||
| | * | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵ | 2017-10-05 | |
| |/ |/| | | | | | | | | | | | | | | | | | | | | | 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega. | ||
* | | Mention requiring extraction/funind in CHANGES | 2017-10-02 | |
| | | |||
| * | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | 2017-09-25 | |
|/ | |||
* | Fix CHANGES after merge of PR #1025. | 2017-09-15 | |
| | |||
* | read flags from project file for Compile Buffer | 2017-09-05 | |
| | |||
* | move mention of native_compute profiling in CHANGES | 2017-09-01 | |
| | |||
* | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | 2017-08-29 | |
|\ | |||
| * | add CHANGES entry | 2017-08-18 | |
| | | |||
* | | Correct the option for cumulativity in CHANGES | 2017-08-18 | |
|/ | |||
* | Use the wording suggested by Gaetan. | 2017-08-17 | |
| | |||
* | Addition suggested by Pierre-Marie. | 2017-08-17 | |
| |