aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge remote-tracking branch 'github/pr/341' into v8.6Gravatar Maxime Dénès2016-11-03
|\ | | | | | | Was PR#341: Better Arguments compatibility.
| * Better Arguments compatibility.Gravatar Maxime Dénès2016-11-02
|/ | | | | With multiple arguments list, repeating the "/" modifier used to be mandatory. So instead of forbidding it, we issue a deprecation warning.
* Fix spurious OCaml Warning 56 in TACTIC EXTEND macros.Gravatar Pierre-Marie Pédrot2016-10-30
|
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-29
|\
* | Removing dead code.Gravatar Hugo Herbelin2016-10-29
| |
* | Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Gravatar Hugo Herbelin2016-10-29
| | | | | | | | (May it fell in the case mentioned in the inner comment of Exninfo.info?)
* | Fixing #5164 (regression in locating error in argument of "refine").Gravatar Hugo Herbelin2016-10-29
| | | | | | | | | | | | Reporting location was not expecting a term passed to an ML tactic to be interpreted by the ML tactic itself. Made an empirical fix to report about the as-precise-as-possible location available.
* | Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \ | | | | | | | | | Was PR#321: Handling of section variables in hints
* \ \ Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \ \ | | | | | | | | | | | | Was PR#319: More error tagging, try to fix bug 5135
* \ \ \ Merge commit 'fccbd64' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \ \ \ | | | | | | | | | | | | | | | Was PR#187: Add a META file to support ocamlfind linking.
| * | | | [build] Add a target to install the META file.Gravatar Emilio Jesus Gallego Arias2016-10-28
| | | | |
| * | | | [build] META file to enable plugin linking with ocamlfind.Gravatar Emilio Jesus Gallego Arias2016-10-28
| | | | | | | | | | | | | | | | | | | | This allows building SerAPI and jsCoq using ocamlbuild.
* | | | | Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Was PR#337: Fix arguments
| | | | | * Fixing #5161 (case of a notation with unability to detect a recursive binder).Gravatar Hugo Herbelin2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations.
| * | | | | Add missing dot to impargs error message.Gravatar Maxime Dénès2016-10-27
| | | | | |
| * | | | | Proper fix for #3753 (anomaly with implicit arguments and renamings)Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of circumventing the problem on the caller's side, as was done in Arguments, we simply avoid failing as there was no real reason for this anomaly to be triggered. If the list of renamings is shorter than the one of implicits, we simply interpret the remaining arguments as not renamed.
| * | | | | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs.
* | | | | | Using msg_info for info_auto and info_eauto (PR #324).Gravatar Hugo Herbelin2016-10-26
| | | | | |
* | | | | | STM: make ~valid state id non optional from APIsGravatar Enrico Tassi2016-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It used to be Stateid.initial by default. That is indeed a valid state id but very likely not the very best one (that would be the tip of the document).
* | | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
|\ \ \ \ \ \ | | |_|_|_|/ | |/| | | |
| * | | | | Merge remote-tracking branch 'github/pr/338' into v8.5Gravatar Maxime Dénès2016-10-25
| |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#338: Remove warning now that info_auto is fixed.
| | * | | | | Remove warning now that info_auto is fixed.Gravatar Théo Zimmermann2016-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Removes a warning dating from 8.5 signaling that info_auto and info_trivial are broken and advising to use Info 1 auto instead. Now, these tactics are fixed and thus they can be used again. They do not do exactly the same thing as Info 1 auto and may be more useful for the learner.
| * | | | | | Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Gravatar Maxime Dénès2016-10-25
| |/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses.
* | | | | | Merge commit 'a799600' into v8.6Gravatar Maxime Dénès2016-10-25
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#334: Fix bug 5031 : should not be an anomaly
| * | | | | | That Function is unable to create a Fixpoint equation is a user problem,Gravatar Yves Bertot2016-10-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | not an anomaly
| | * | | | | Update CHANGES.Gravatar Maxime Dénès2016-10-25
| | | | | | |
| | * | | | | Bump version number to 8.5pl3.Gravatar Maxime Dénès2016-10-25
| | | | | | |
| | * | | | | Merge remote-tracking branch 'github/pr/333' into v8.5Gravatar Maxime Dénès2016-10-25
| | |\ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | Was PR#233: Fix a bug in error printing of unif constraints
| | * \ \ \ \ \ Merge remote-tracking branch 'github/pr/329' into v8.5Gravatar Maxime Dénès2016-10-25
| | |\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#329: Fix #5127 Memory corruption with the VM
* | | \ \ \ \ \ \ Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-24
|\ \ \ \ \ \ \ \ \ | | |/ / / / / / / | |/| | | | | | |
* | | | | | | | | Adding a test for #4398 (interpretation scopes for "match goal").Gravatar Hugo Herbelin2016-10-24
| | | | | | | | |
* | | | | | | | | Rename lia.cache into .lia.cache in the test-suite Makefile.Gravatar Maxime Dénès2016-10-24
| | | | | | | | |
* | | | | | | | | Merge commit '81bdc22' into v8.6Gravatar Maxime Dénès2016-10-24
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#301: Update .gitignore with new names for psatz caches.
| | * \ \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/326' into v8.5Gravatar Maxime Dénès2016-10-24
| | |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#326: Extend documentation of auto
| | | | | * | | | | | Test file for #5127: Memory corruption with the VMGravatar Maxime Dénès2016-10-24
| | | | | | | | | | |
| | | | | * | | | | | Fix #5127 Memory corruption with the VMGravatar Maxime Dénès2016-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bytecode interpreter ensures that the stack space available at some points is above a static threshold. However, arbitrary large stack space can be needed between two check points, leading to segmentation faults in some cases. We track the use of stack space at compilation time and add an instruction to ensure greater stack capacity when required. This is inspired from OCaml's PR#339 and PR#7168. Patch written with Benjamin Grégoire.
* | | | | | | | | | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | + a few improvements on 5f1dd4c40 (lexing of { and }).
* | | | | | | | | | | ssrmatching: fix interpretation of rpatternGravatar Enrico Tassi2016-10-24
| |_|_|/ / / / / / / |/| | | | | | | | |
| | * | | | | | | | Fixing a location bug with "?" and "$".Gravatar Hugo Herbelin2016-10-24
| | | | | | | | | |
| | * | | | | | | | Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").Gravatar Hugo Herbelin2016-10-24
| | | |/ / / / / / | | |/| | | | | |
| * | | | | | | | Update .gitignore with new names for psatz cachesGravatar Jason Gross2016-10-24
| | | | | | | | |
| | * | | | | | | Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong.Gravatar Hugo Herbelin2016-10-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | New fix. A bit less consistent with the spirit of this Makefile as we list prerequisite files explicitly, but avoid to redo subsystems at each call to "make" as with previous fix. Other solutions from experts are welcome.
* | | | | | | | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-22
|\ \ \ \ \ \ \ \ \ | | |/ / / / / / / | |/| | | | | | |
| * | | | | | | | Remove incorrect assertion in cbn (bug #4822).Gravatar Guillaume Melquiond2016-10-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion).
| * | | | | | | | Do not stop propagation of signals when Coq is busy (bug #3941).Gravatar Guillaume Melquiond2016-10-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted.
| * | | | | | | | Fix incorrect token description for bullets.Gravatar Guillaume Melquiond2016-10-22
| | | | | | | | |
| * | | | | | | | Fixing printing of generic arguments of tag "var".Gravatar Hugo Herbelin2016-10-22
| | | | | | | | |
| | | | * | | | | Fix a bug in error printing of unif constraintsGravatar Matthieu Sozeau2016-10-22
| | |_|/ / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conversion problems are in a de Bruijn environment that may include references to unbound rels (because of the way evars are created), we patch the env to named all de Bruijn variables so that error printing does not raise an anomaly. Also fix a minor printing bug in unsatisfiable constraints error reporting. HoTT_coq_117.v tests all of this.
* | | | | | | | Adding a test for bug #3495.Gravatar Pierre-Marie Pédrot2016-10-21
| | | | | | | |
* | | | | | | | Oops, my bad, didn't expect a merge issue!Gravatar Matthieu Sozeau2016-10-21
| | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 22:25:27 +0000