| Age | Commit message (Collapse) | Author |
|---|
|
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
|
|
|
|
Removing blocking of generalization on destructed hypothesis
introduced on Nov 2. It was a bad idea as shown by bug #3790 on
eliminating v:Vector n, keeping an equality.
|
|
|
|
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.
|
|
|
|
|
|
(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.)
|
|
|
|
- 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).
|
|
(the action is "clear").
Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.
Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
|
|
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
|
|
3566 gave a legitimate error, keyedrewrite was not setting keyed
unification on.
|
|
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
|
|
|
|
|
examples.
|
|
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
|
|
|
|
of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).
|
|
|
|
generated equation names).
|
|
implicits do not allow to parse as an application and cleanup code.
|
|
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.
|
|
|
|
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
fresh names interferring with names later generated in intropatterns
(as introduced in 72498d6d68ac which passed "clenv_refine_in continued
by pattern introduction" to descend_in_conjunction while only a pure
clenv_refine was passed before). The 72498d6d68ac version was
generating fresh names in the wrong order (morally-private names for
descend_in_conjunction before user-level names in clenv_refine_in).
The 19a7a5789c fix was introducing expressions not handled by the
refine from logic.ml.
In particular, this fixes RelationAlgebra.
|
|
|
|
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
|
at least remove the successes obtained by trivial unification of a
meta with the goal, so as to avoid surprising results. We generalize
this to variables which will only eventually be replaced by metas.
|
|
presence of let-ins.
|
