| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |\|
| |
| |
| | |
Did some manual merge in tactics/tactics.ml.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
inconsistent).
|
| |\| |
|
| | |
| |
| |
| | |
universes are declared correctly in the enclosing proofs evar_map's.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
After all, let's target 8.6.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
of the return clause and of the branches (what assumed that the
implementation preserves the invariant that the return predicate and
the branches are in canonical [fun Δ => t] form, with Δ possibly
containing let-ins).
|
| |\| |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).
Interpretation was corrected, but error message was damaged.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- "Proof using p*" means: use p and any section var about p.
- Simplify the grammar/parser for proof using <expression>.
- Section variables with a body (let-in) are pulled in automatically
since they are safe to be used (add no extra quantification)
- automatic clear of "unused" section variables made optional:
Set Proof Using Clear Unused.
since clearing section hypotheses does not "always work" (e.g. hint
databases are not really cleaned)
- term_typing: trigger a "suggest proof using" message also for Let
theorems.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.
|
| |\| |
|
| | |
| |
| |
| | |
of temporary hypotheses than 76f27140e6e34 did.
|
| |\| |
|
| | |
| |
| |
| |
| | |
ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).
|
| | |
| |
| |
| |
| |
| |
| |
| | |
an initial hypothesis hyp at the same position in the context.
Ensuring the same for "apply c in hyp as pat".
Ensuring that "pose proof (H ...) as H" does not change the position of H.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
Use expand projection to come back to the projection-as-constant encoding, dealing with parameters correctly.
|
| |\| |
|
| | |
| |
| |
| |
| | |
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
|
| | |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
| | | |
|
| |\|
| |
| |
| |
| |
| |
| | |
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
| | |
| |
| |
| |
| |
| |
| |
| | |
The ~polyprop argument wasn't propagated properly anymore,
leading the extraction to try to operate on situations it cannot
handle (yet). Cf Table.error_singleton_become_prop for more details.
Regression test added.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
|
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau
Maxime Dénès
Guillaume Melquiond
Enrico Tassi
Matthieu Sozeau
Pierre Letouzey