| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
|
| |
on vm and #3068 by Nov 2 commit on destruct.
Also fixed test for failure of #3459.
|
| |
|
|
|
| |
for residual unifiable evars (otherwise "thin" from logic.ml, erases
the src field) + typo.
|
| |
|
|
|
| |
intrusive residual local definitions + more conservative strategy for
which variables are not generalized (point 2 of 4df1ddc6d6bd07073).
|
| |
|
|
| |
local definitions...
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- It removes some redundancies.
- It fixes failures when destructing a term mentioning goal hypotheses
x1, ..., xn or a term which is a section variable x when this term
is in a type with indices, and the indices also occur in the type of
one of x1, ..., xn, or of x.
- It fixes non-respect of eliminator type when completing pattern possibly
given by a prefix.
- It fixes b2e1d4ea930c which was dealing with the case when the term
was a section variable (it was unfortunately also breaking some
compatibility about which variables variable were generalized in
induction and which variables were automatically cleared because
unselected).
|
| | |
|
| |
|
|
|
|
|
| |
This is now a "like first" strategy iff there is no occurrences
selected in either the goal or in one of the hypotheses possibly given
in an "in" clause. Before, it was "like first" if and only if no "in"
clause was given at all.
|
| | |
|
| |
|
|
|
|
|
| |
Need some contorsion for not using the general scheme of naming based
which uses the hypothesis name as base ident, and for instead keeping
a name generated on the type of the section variable, as it was before
for section variables (example of incompatibility in FMapPositive).
|
| |
|
|
|
|
|
| |
keeping them as open holes. When these arguments are class instances,
this restores compatibility with the 8.4 search for subterms from
non-fully applied patterns which was using conversion on the
instances.
|
| |
|
|
|
|
|
| |
dependent in the goal without being fully applied: it cannot be
erased. This used to work in 8.4 when the hypothesis was in an empty
type. I fixed this and (somehow arbitrarily) generalized the
non-erasing to other inductive types instead of failing.
|
| | |
|
| |
|
|
|
|
| |
that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
in goal context.
Note: printing of a declaration was previously done in the context
made of the preceding segment of hypotheses, while now it is made in
the full context of all hyps (those coming before and after the hyp
being printed). As a consequence, constants which could be confused
with a variable in the context are now always qualified even if the
conflicting variable name is coming later. But why not, that looks
somehow more uniform like this.
|
| | |
|
| |
|
|
| |
Was always failing due to an incorrect use of Ltac's or.
|
| | |
|
| |
|
|
| |
the printing of the context of open evars in Check.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.
This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.
Another part is still open (see test-suite).
|
| |
|
|
|
|
|
|
|
|
|
| |
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc).
It may be the case that the new expression lives in a higher sorts and
the context where it is substituted in supports it. So, it is too
strong to expect that, when the substituted objects are types, the
sort of the new one is smaller than the sort of the original
one. Consider e.g.
Goal @eq Type nat nat.
change nat with (@id Type nat).
which is a correct replacement, even if (id Type nat) is in a higher sort.
Introducing typing in "contextually" would be a big change for a
little numbers of uses, so we instead (hackily) recheck the whole term
(even though typing with evars uses evar_conv which accept to unify
Type with Set, leading to wrongly accept "Goal @eq Set nat nat.
change nat with (@id Type nat).". Evar conv is however rejecting
Prop=Type.)
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
projections in cbv when delta _and_ beta flags are set. Add test-suite
file for bug 3700 too.
|
| |
|
|
|
| |
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
now fails with Error: Already an existential evar of name Main
|
| | |
|
| |
|
|
|
|
| |
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
|
| |
|
|
| |
of the record binder for Class C's projections.
|
| |
|
|
|
| |
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
|
| |
|
|
| |
unification.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
2nd-order matching).
We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is
well-typed when taking the filtered context Gamma) in 2nd order
matching. Maybe this weakens the power of the 2nd order matching
algorithm, so it is not clear that it is the good fix.
Another fix could have been to ensure that taking the closure of
filter does not extend it beyond the original filter (hence keeping
the filter untyped if it was already untyped).
As for the bug #3045, it also revealed that some "destruct c as [[]]"
could be made stronger as decomposing the destruct in two parts
"destruct c as [x]; destruct x" workis while it currently fails if in
one part.
|
| | |
|
| | |
|
| |
|
|
| |
condition.
|
| |
|
|
|
|
|
|
| |
- Optimize the removal of generalization when there is no dependency in
the generalized variable (see postprocess_dependencies, and the removal
of dependencies in the default type of impossible cases).
- Compute the onlydflt flag correctly (what allows automatic treatment
of impossible cases even when there is no clause at all).
|
| | |
|
| | |
|
| |
|
|
|
| |
type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).
|
Xavier Clerc
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Matthieu Sozeau