aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* 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
* | 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
|\
| * 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
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 05:27:23 +0000