| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
| |
(It was reducing also in hypotheses.)
|
| |
|
|
|
|
|
|
| |
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 done with Enrico.
|
|
|
|
|
|
| |
csdp.cache -> .csdp.cache
lia.cache -> .lia.cache
nlia.cache -> .nia.cache
|