| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
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).
|
|
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.
|
|
|
|
|
|
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.
|
|
Was PR#328: Change the order of arguments of fig2dev.
|
|
|
|
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".
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
|
|
|
|
"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.
|
|
Header was missing in last commit.
One day, it would be nice to unify the display of "debug auto" and
"debug eauto"...
|
|
|
|
This happens when recursive notations are used to define recursive
notations.
|
|
Was PR#286: Fix the definition of if_then_else for tactics with multiple
success.
|
|
|
|
|
|
|
|
Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
|
|
side_effects. Partial solution to the handling of side effects
in proofview.
|
|
|
|
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).
|
|
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).
|
|
#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 was made precociously dependent on user-declared reduction
behaviors. Only cbn should rely on that.
|
|
This change exposed bug #4763
|
|
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.
|
|
|
|
if_then_else definition does not account for multi success tactics.
tryif_then_else is a primitive tactical with the expected behavior.
|
|
|
|
Restore subst output test file modified by mistake.
|
|
Was PR#294: Make error message more helpful.
|
|
Was PR#293: Fix #4762 (eauto weaker than auto).
|
|
|
|
|
|
CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
|
|
|
|
the case for clear and the conversion tactics.
|
|
|
|
as suggested by Hugo. Also, escape the spaces after the dots to obtain
a better PdfLaTeX output.
|
|
- 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.
|
|
|
|
|
|
|
