| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-01-23 | Merge PR #6629: Archive COMPATIBILITY | Maxime Dénès | |
| 2018-01-22 | Move the mention of the removal of Qed exporting at the right place. | Théo Zimmermann | |
| 2018-01-22 | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction. | Maxime Dénès | |
| 2018-01-18 | add flash infos about wrap, not found, no. of replacements, no. of finds, ↵ | Paul Steckler | |
| issue #6452 | |||
| 2018-01-18 | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder. | Maxime Dénès | |
| 2018-01-17 | Add CHANGES entry | Jasper Hugunin | |
| 2018-01-17 | Add CHANGES entry | Jasper Hugunin | |
| 2018-01-16 | Merge PR #6551: Bracket with goal selector | Maxime Dénès | |
| 2018-01-05 | Documentation and CHANGES for bracket with goal selector. | Théo Zimmermann | |
| 2018-01-03 | add optimize_heap tactic for #6488 | Paul Steckler | |
| 2017-12-20 | Merge PR #6377: Removal of the FAQ LaTex document. | Maxime Dénès | |
| 2017-12-18 | Merge PR #6381: A version of [time] that works on constr evaluation | Maxime Dénès | |
| 2017-12-18 | Merge PR #6380: Add tactics to reset and display the Ltac profile | Maxime Dénès | |
| 2017-12-18 | Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in ↵ | Maxime Dénès | |
| Extraction Language command | |||
| 2017-12-18 | Removing the FAQ, which has been moved to the GitHub wiki for this | Matt Quinn | |
| repository. Also removing FAQ-related build rules. | |||
| 2017-12-15 | Merge PR #6429: 8.7.1 CHANGES. | Maxime Dénès | |
| 2017-12-14 | Add documentation for time_constr | Jason Gross | |
| 2017-12-14 | Add doc+changelog entries for new LtacProf tactics | Jason Gross | |
| 2017-12-14 | 8.7.1 CHANGES. | Théo Zimmermann | |
| 2017-12-12 | In printing, factorizing "match" clauses with same right-hand side. | Hugo Herbelin | |
| 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... | |||
| 2017-12-07 | Merge PR #873: New strategy based on open scopes for deciding which notation ↵ | Maxime Dénès | |
| to use among several of them | |||
| 2017-12-05 | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | Paul Steckler | |
| 2017-12-01 | Update CHANGES | Matthieu Sozeau | |
| 2017-12-01 | Merge PR #6276: Coqchk accepts filenames | Maxime Dénès | |
| 2017-11-29 | Remove "obsolete_locality" and fix STM vernac classification. | Maxime Dénès | |
| 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. | |||
| 2017-11-29 | Documenting the possibility to pass filenames to coqchk. | Pierre-Marie Pédrot | |
| 2017-11-27 | Selecting which notation to print based on current stack of scope. | Hugo Herbelin | |
| See discussion on coq-club starting on 23 August 2016. An open question: what priority to give to "abbreviations"? | |||
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | |
| 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. | |||
| 2017-10-19 | Moving bug numbers to BZ# format in the CHANGES file. | Théo Zimmermann | |
| Compared to the original proposition (ba7fa6b in #960), this commit only re-formats bug numbers that are also PR numbers. | |||
| 2017-10-10 | Merge PR #540: [configure] Support for flambda flags. | Maxime Dénès | |
| 2017-10-10 | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès | |
| 2017-10-10 | [configure] Support for flambda flags. | Emilio Jesus Gallego Arias | |
| We add a new option to configure `-flambda-opts` to allow passing custom flags to flambda. Example: ``` ./configure -flambda-opts "-O3 -unbox-closures" ``` | |||
| 2017-10-09 | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵ | Maxime Dénès | |
| printing-ony Notations | |||
| 2017-10-06 | 8.7+beta2 CHANGES | Théo Zimmermann | |
| 2017-10-05 | romega: takes advantage of context variables with body | Pierre Letouzey | |
| 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). | |||
| 2017-10-05 | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵ | Pierre Letouzey | |
| 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. | |||
| 2017-10-02 | Mention requiring extraction/funind in CHANGES | Tej Chajed | |
| 2017-09-25 | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | |
| 2017-09-15 | Fix CHANGES after merge of PR #1025. | Théo Zimmermann | |
| 2017-09-05 | read flags from project file for Compile Buffer | Paul Steckler | |
| 2017-09-01 | move mention of native_compute profiling in CHANGES | Paul Steckler | |
| 2017-08-29 | Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170 | Maxime Dénès | |
| 2017-08-18 | add CHANGES entry | Paul Steckler | |
| 2017-08-18 | Correct the option for cumulativity in CHANGES | Amin Timany | |
| 2017-08-17 | Use the wording suggested by Gaetan. | Théo Zimmermann | |
| 2017-08-17 | Addition suggested by Pierre-Marie. | Théo Zimmermann | |
| 2017-08-16 | Additions following Hugo's suggestions. | Théo Zimmermann | |
| 2017-08-16 | Improve wording. | Théo Zimmermann | |
| 2017-08-16 | 8.7 CHANGES | Théo Zimmermann | |
| 2017-08-16 | Porting #856 (8.6.1 CHANGES entries) to master | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |