aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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).
| | * Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵Gravatar Pierre Letouzey2017-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 CHANGESGravatar Tej Chajed2017-10-02
| |
| * BZ#5739, Allow level for leftmost nonterminal for printing-ony NotationsGravatar Paul Steckler2017-09-25
|/
* Fix CHANGES after merge of PR #1025.Gravatar Théo Zimmermann2017-09-15
|
* read flags from project file for Compile BufferGravatar Paul Steckler2017-09-05
|
* move mention of native_compute profiling in CHANGESGravatar Paul Steckler2017-09-01
|
* Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170Gravatar Maxime Dénès2017-08-29
|\
| * add CHANGES entryGravatar Paul Steckler2017-08-18
| |
* | Correct the option for cumulativity in CHANGESGravatar Amin Timany2017-08-18
|/
* Use the wording suggested by Gaetan.Gravatar Théo Zimmermann2017-08-17
|
* Addition suggested by Pierre-Marie.Gravatar Théo Zimmermann2017-08-17
|
* Additions following Hugo's suggestions.Gravatar Théo Zimmermann2017-08-16
|
* Improve wording.Gravatar Théo Zimmermann2017-08-16
|
* 8.7 CHANGESGravatar Théo Zimmermann2017-08-16
|
* Porting #856 (8.6.1 CHANGES entries) to masterGravatar Théo Zimmermann2017-08-16
|
* Merge PR #925: Document Extraction TestCompileGravatar Maxime Dénès2017-08-01
|\
| * Extraction TestCompile documented + mentionned in CHANGESGravatar Pierre Letouzey2017-07-27
| | | | | | | | Also includes a minor fix of the Extraction doc (a Require was missing).
* | Adding support for recursive notations of the form "x , .. , y , z".Gravatar Hugo Herbelin2017-07-26
|/ | | | | | | | | Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing.
* Add an entry to CHANGES about timing in coq_makefileGravatar Jason Gross2017-07-11
|
* Update CHANGES with inversion_sigma entryGravatar Jason Gross2017-06-30
|
* Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\
| * [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
* | Document cumulativity for inductive typesGravatar Amin Timany2017-06-16
|/
* BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Gravatar Pierre Letouzey2017-06-13
| | | | | | See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude.
* Merge PR#709: Bytecode compilation apart from 'make world', againGravatar Maxime Dénès2017-06-12
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 21:39:50 +0000