| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| | |
"Fetching opaque proofs" notices are not printed by default anymore.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
I don't know what was the intent of Pierre B here. In 8.4, it was not
supported, raising with an error at parsing time. I changed the
anomaly into an error at interpretation time, so it is still not
supported but we could support it if some legitimate use of it
eventually appears.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
of syntax in test file ltac.v.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
capturing bound names unexpectingly).
We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").
We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in
let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).
which was producing
forall z : nat, match z with 0 => z | S y => y end = 0
because the names in default branches are treated specifically.
It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).
However, we rename binders in fix which were not interpreted.
There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).
fix ltac name
|
| | |
| |
| |
| |
| |
| |
| | |
considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).
Also updating and fixing wrong comments in test apply.v.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
breaking backtracking in the presence of functors).
In "interactive" rather than "bugs" because of the use of Back.
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
abbreviation not bound to an applied constructor as itself but rather
as a binding variable as it was the case for non-applied
constructor). This was broken by e5c02503 while fixed #3483 (Not_found
uncaught with a notation to a non-constructor).
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
|
| | | |
|
| | |
| |
| |
| |
| | |
former filter after 48509b61 and 3cd718c, because filtered let-ins
were not any longer preserved).
|
| | | |
|
| | |
| |
| |
| |
| | |
Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
|
| | |
| |
| |
| |
| |
| |
| | |
Fixes bug #4176 (actually two bugs in one)
Correct computation of the type of primitive projections in presence of
let-ins.
|
| | |
| |
| |
| |
| | |
Adapt to new [projection] abstract type comprising a constant and
a boolean.
|
| | |
| |
| |
| |
| | |
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
|
| | |
| |
| |
| |
| | |
Using relative path for coqlib, for some reason this fails on Mac OS
X. Took the easiest way to fix it.
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Triggers a bug in declarative mode. Waiting for someone to volunteer and fix
the bug, but meanwhile I'm trying to fix the test-suite.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
A possible script breakage can occur if one has a notation
at level 11 that is also right associative (now 11 is left associative).
Thanks Georges for debugging that.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
In case we need to backtrack on universe inconsistencies when converting
two (incompatible) instances of the same constant and unfold them.
Bug reported by Amin Timany.
|
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Guillaume Melquiond
Matthieu Sozeau
Matthieu Sozeau
Enrico Tassi