aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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
|/
* 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
|\
| * mention 'make world' without 'byte' in CHANGES + 2 minor suggestionsGravatar Pierre Letouzey2017-06-01
| |
* | Merge PR#449: make specialize smarter (bug 5370).Gravatar Maxime Dénès2017-06-01
|\ \
| * | Tests for new specialize feature + CHANGES.Gravatar Pierre Courtieu2017-05-31
| |/
* / Documentation for eassert, eenough, epose proof, eset, eremember, epose.Gravatar Hugo Herbelin2017-05-30
|/ | | | Includes fixes and suggestions from Théo.
* Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \
| * | enters coq_makefile2Gravatar Enrico Tassi2017-05-23
| | |
* | | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
| * Clarifying the interpretation path for the "constr_with_binding" argument.Gravatar Hugo Herbelin2017-05-22
|/ | | | | | | | | | | | | | | | | This fixes an inconsistency introduced in 554a6c806 (svn r12603) where both interp_constr_with_bindings and interp_open_constr_with_bindings were going through interp_open_constr (no type classes so as to not to commit too early on irreversible choices, accepting unresolved holes). We fix this by having interp_constr_with_bindings going to interp_constr (using type classes and failing on unresolved evars). The external impact is that any TACTIC EXTEND which refers to constr_with_binding has now to decide whether it intends it to use what the name suggest (using type classes and to fail if evars remain unresolved), thus keeping constr_with_binding, or the actual behavior which requires to use open_constr_with_bindings for strict compatibility.
* Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
|\
* | Aligning on standard layout of CHANGES.Gravatar Hugo Herbelin2017-05-13
| |
| * Documenting Printing Compact Contexts + CHANGESGravatar Pierre Courtieu2017-05-11
| |
* | Tentative note in CHANGES about now applying βι while typing "match" branches.Gravatar Hugo Herbelin2017-04-27
|/ | | | | | | In practice, this is almost invisible except when using "refine". So, in some sense, it is aligning the behavior of pretyping on the one of logic.ml's "refine" so that the more natural behavior of 8.4's refine on this issue is restored.
* CHANGES entry for #545.Gravatar Maxime Dénès2017-04-19
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 11:17:05 +0000