aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixing to #3209 (Not_found due to an occur-check cycle).Gravatar Hugo Herbelin2016-10-17
| | | | | | | The fix solves the original bug report but it only turns the Not_found into a normal error in the alternative example by Guillaume. See test-suite file for comments on how to eventually improve the situation and find a solution in Guillaume's example too.
* Fixing a missing constraint in consider_remaining_unif_constraints.Gravatar Hugo Herbelin2016-10-17
|
* Merge PR #310 into v8.5Gravatar Pierre-Marie Pédrot2016-10-17
|\
| * Test for bug #4874.Gravatar Pierre-Marie Pédrot2016-10-17
| |
* | Still a problem with debug auto printing.Gravatar Hugo Herbelin2016-10-15
| | | | | | | | | | "msg_debug (mt())" is not identity, so we return back to how it was done in 8.4, contracting a repeated pattern-matching into one.
* | One more little bug in the output of "debug auto".Gravatar Hugo Herbelin2016-10-15
| | | | | | | | | | | | | | Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"...
* | Fixing printing of info_auto broken since 0091c528 (2014).Gravatar Hugo Herbelin2016-10-14
| |
* | Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-10-12
| | | | | | | | | | This happens when recursive notations are used to define recursive notations.
* | Merge remote-tracking branch 'github/pr/286' into v8.5Gravatar Maxime Dénès2016-10-12
|\ \ | | | | | | | | | | | | Was PR#286: Fix the definition of if_then_else for tactics with multiple success.
* \ \ Merge remote-tracking branch 'git/bug5123' into v8.5Gravatar Matthieu Sozeau2016-10-12
|\ \ \
| * | | Fix test-suite file 5123 to fail in case of regressionGravatar Matthieu Sozeau2016-10-11
| | | |
* | | | Merge remote-tracking branch 'github/bug4863' into v8.5Gravatar Matthieu Sozeau2016-10-11
|\ \ \ \
| | * | | Fix bug #5123: mark all shelved evars unresolvableGravatar Matthieu Sozeau2016-10-11
| |/ / / |/| | | | | | | | | | | | | | | Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
| * | | Fix for bug #4863, update the Proofview's env withGravatar Matthieu Sozeau2016-10-11
|/ / / | | | | | | | | | | | | side_effects. Partial solution to the handling of side effects in proofview.
* | | Add test file for #4416.Gravatar Maxime Dénès2016-10-10
| | |
* | | Fix #4416: - Incorrect "Error: Incorrect number of goals"Gravatar Arnaud Spiwack2016-10-10
| | | | | | | | | | | | | | | | | | | | | | | | In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
* | | A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Gravatar Hugo Herbelin2016-10-09
| | | | | | | | | | | | | | | | | | | | | More precisely, commands that calls parse_entry put the lexer in an inconsistent state, breaking the lexing of bullet which relies on it. (Not to be pushed to v8.6 which has a better fix).
| | * Revert "Make the pretty printer resilient to incomplete nametab (progress on ↵Gravatar Théo Zimmermann2016-10-06
| |/ |/| | | | | | | | | | | | | | | | | #4363)." This reverts commit 11ccb7333c2a82d59736027838acaea2237e2402. This fixes bug #4874. We fallback to the original error message of v8.4. The fallback printer introduced in this commit only gave unqualified names, which is what this bug reports.
* | evarconv.ml: Fix bug #4529, primproj unfoldingGravatar Matthieu Sozeau2016-10-06
| | | | | | | | | | Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
* | w_merge: Add a comment about the (List.rev evars)Gravatar Matthieu Sozeau2016-10-06
| | | | | | | | This change exposed bug #4763
* | unification.ml: fix for bug #4763, unif regressionGravatar Matthieu Sozeau2016-10-06
| | | | | | | | | | | | | | Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.
* | Fixing #4970 (confusion between special "{" and non special "{{" in notations).Gravatar Hugo Herbelin2016-10-03
| |
| * Remove if_then_else. Use tryif instead.Gravatar Théo Zimmermann2016-10-03
|/ | | | | if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
* Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Gravatar Hugo Herbelin2016-09-30
|
* Fix test-suite.Gravatar Maxime Dénès2016-09-30
| | | | Restore subst output test file modified by mistake.
* Merge remote-tracking branch 'github/pr/294' into v8.5Gravatar Maxime Dénès2016-09-30
|\ | | | | | | Was PR#294: Make error message more helpful.
* \ Merge branch '4762' into v8.5Gravatar Maxime Dénès2016-09-30
|\ \ | | | | | | | | | Was PR#293: Fix #4762 (eauto weaker than auto).
| * | Fix #4762.Gravatar Cyprien Mangin2016-09-30
| | |
* | | Fix a bug in subst releaved by an OCaml warning.Gravatar Maxime Dénès2016-09-29
|/ /
| * Make error message more helpful.Gravatar Théo Zimmermann2016-09-28
|/ | | CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
* Fixing #4887 (confusion between using and with in documentation of firstorder).Gravatar Hugo Herbelin2016-09-27
|
* Ensuring that the evar name is preserved by "rename" as it is alreadyGravatar Hugo Herbelin2016-09-24
| | | | the case for clear and the conversion tactics.
* Fixing #5095 (non relevant too strict test in let-in abstraction).Gravatar Hugo Herbelin2016-09-22
|
* Replace { command ; } with ( command )Gravatar Erik Martin-Dorel2016-09-19
| | | | | as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output.
* Fix typos in RefMan-uti.tex.Gravatar Erik Martin-Dorel2016-09-19
| | | | | | - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace.
* Fixing test-suite after commit 43104a0b.Gravatar Pierre-Marie Pédrot2016-09-14
|
* Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
|
* Test for #5077.Gravatar Hugo Herbelin2016-09-10
|
* Fixing #5077 (failure on typing a fixpoint with evars in its type).Gravatar Hugo Herbelin2016-09-10
| | | | | Typing.type_of was using conversion for types of fixpoints while it could have used unification.
* Restore native compiler optimizations after they were broken by 9e2ee58.Gravatar Maxime Dénès2016-09-09
| | | | | | | | The greatest danger of OCaml's polymorphic equality is that PMP can replace it with pointer equality at any time, be warned :) The lack of optimization may account for an exponential blow-up in size of the generated code, as well as worse runtime performance.
* Test file for #5065 - Anomaly: Not a proof by inductionGravatar Maxime Dénès2016-09-05
|
* Fix #5065: Anomaly: Not a proof by inductionGravatar Maxime Dénès2016-09-05
| | | | | | Using abstract can create beta-redexes or let-ins in the head of the proof terms. The code projecting out mutual lemmas was not robust enough.
* Fixing what is probably a typo in Strict Proofs mode (#5062).Gravatar Hugo Herbelin2016-09-03
|
* Fix test-suite after Frédéric's 6231f07b2.Gravatar Maxime Dénès2016-09-01
|
* Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior).Gravatar Hugo Herbelin2016-09-01
| | | | (It was reducing also in hypotheses.)
* Fixing name of internal refine ("simple refine").Gravatar Hugo Herbelin2016-09-01
|
* Fix bug #5043: [Admitted] lemmas pick up section variables.Gravatar Pierre-Marie Pédrot2016-08-31
| | | | | | We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
* Fix #4871 - interrupting par:abstract kills coqtopGravatar Maxime Dénès2016-08-30
| | | | Fix done with Enrico.
* micromega cache files are now hidden files (cf #4156)Gravatar Frédéric Besson2016-08-30
| | | | | | csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache
* Setting an unknown option now always a warning. Fixes #4947.Gravatar Maxime Dénès2016-08-30
| | | | | | | | Previously, setting an unknown option was an error or a warning, depending on the type of the option. We make it always a warning, for forward compatibility. This was already fixed in 8.6.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 22:20:52 +0000