aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-10-22Fixing printing of generic arguments of tag "var".Hugo Herbelin
2016-10-21Revert "unification.ml: fix for bug #4763, unif regression"Maxime Dénès
This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a. A good fix requires to review a bit the design of unification constraint postponement, which we do in 8.6. We leave things as they are in 8.5 for compatibility.
2016-10-21Merge remote-tracking branch 'github/pr/328' into v8.5Maxime Dénès
Was PR#328: Change the order of arguments of fig2dev.
2016-10-20Adding dependency of the test-suite subsystems in prerequisite (fixing #5150).Hugo Herbelin
2016-10-20A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).Hugo Herbelin
If an existing evar was cleared in pretyping (typically while processing "ltac:"), it created an evar considered as new. Updating them instead along the "cleared" flag. If correct, I suspect similar treatment should be done for refining along "change", "rename" and "move".
2016-10-19Change the order of arguments of fig2dev.Théo Zimmermann
For some reason, with my version of transfig (which seems to be the latest), the order of arguments of the fig2dev command matters: -L png must come before -m 2. I suppose that this fix shouldn't break things for others.
2016-10-18Removing output test for module qualification.Pierre-Marie Pédrot
I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there.
2016-10-17Fixing to #3209 (Not_found due to an occur-check cycle).Hugo Herbelin
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.
2016-10-17Fixing a missing constraint in consider_remaining_unif_constraints.Hugo Herbelin
2016-10-17Merge PR #310 into v8.5Pierre-Marie Pédrot
2016-10-17Test for bug #4874.Pierre-Marie Pédrot
2016-10-15Still a problem with debug auto printing.Hugo Herbelin
"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.
2016-10-15One more little bug in the output of "debug auto".Hugo Herbelin
Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"...
2016-10-14Fixing printing of info_auto broken since 0091c528 (2014).Hugo Herbelin
2016-10-12Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
This happens when recursive notations are used to define recursive notations.
2016-10-12Merge remote-tracking branch 'github/pr/286' into v8.5Maxime Dénès
Was PR#286: Fix the definition of if_then_else for tactics with multiple success.
2016-10-12Merge remote-tracking branch 'git/bug5123' into v8.5Matthieu Sozeau
2016-10-11Fix test-suite file 5123 to fail in case of regressionMatthieu Sozeau
2016-10-11Merge remote-tracking branch 'github/bug4863' into v8.5Matthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-10Add test file for #4416.Maxime Dénès
2016-10-10Fix #4416: - Incorrect "Error: Incorrect number of goals"Arnaud Spiwack
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).
2016-10-09A tentative fix for #5102 (bullets parsing broken by calls to parse_entry).Hugo Herbelin
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).
2016-10-06Revert "Make the pretty printer resilient to incomplete nametab (progress on ↵Théo Zimmermann
#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.
2016-10-06evarconv.ml: Fix bug #4529, primproj unfoldingMatthieu Sozeau
Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
2016-10-06w_merge: Add a comment about the (List.rev evars)Matthieu Sozeau
This change exposed bug #4763
2016-10-06unification.ml: fix for bug #4763, unif regressionMatthieu Sozeau
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.
2016-10-03Fixing #4970 (confusion between special "{" and non special "{{" in notations).Hugo Herbelin
2016-10-03Remove if_then_else. Use tryif instead.Théo Zimmermann
if_then_else definition does not account for multi success tactics. tryif_then_else is a primitive tactical with the expected behavior.
2016-09-30Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Hugo Herbelin
2016-09-30Fix test-suite.Maxime Dénès
Restore subst output test file modified by mistake.
2016-09-30Merge remote-tracking branch 'github/pr/294' into v8.5Maxime Dénès
Was PR#294: Make error message more helpful.
2016-09-30Merge branch '4762' into v8.5Maxime Dénès
Was PR#293: Fix #4762 (eauto weaker than auto).
2016-09-30Fix #4762.Cyprien Mangin
2016-09-29Fix a bug in subst releaved by an OCaml warning.Maxime Dénès
2016-09-28Make error message more helpful.Théo Zimmermann
CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
2016-09-27Fixing #4887 (confusion between using and with in documentation of firstorder).Hugo Herbelin
2016-09-24Ensuring that the evar name is preserved by "rename" as it is alreadyHugo Herbelin
the case for clear and the conversion tactics.
2016-09-22Fixing #5095 (non relevant too strict test in let-in abstraction).Hugo Herbelin
2016-09-19Replace { command ; } with ( command )Erik Martin-Dorel
as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output.
2016-09-19Fix typos in RefMan-uti.tex.Erik Martin-Dorel
- 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.
2016-09-14Fixing test-suite after commit 43104a0b.Pierre-Marie Pédrot
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-09-10Test for #5077.Hugo Herbelin
2016-09-10Fixing #5077 (failure on typing a fixpoint with evars in its type).Hugo Herbelin
Typing.type_of was using conversion for types of fixpoints while it could have used unification.
2016-09-09Restore native compiler optimizations after they were broken by 9e2ee58.Maxime Dénès
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.
2016-09-05Test file for #5065 - Anomaly: Not a proof by inductionMaxime Dénès
2016-09-05Fix #5065: Anomaly: Not a proof by inductionMaxime Dénès
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.
2016-09-03Fixing what is probably a typo in Strict Proofs mode (#5062).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 20:59:09 +0000