| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
while before these were supposed to consider only syntactically.
Made the experiment to unify with all delta flags unset. Keeping the
same flags as for non evar/meta free subterms would lead to too much
successes, as e.g. "true && b" matching "b" when the
modulo_conv_on_closed_terms flag is set, which is the case for
rewrite. But maybe should we instead investigate to have the same
flags but with the restrict_conv_on_strict_subterms flag set. This
rules out examples like "true && b" unifying with "b" and this is
another option which is ok for compiling the stdlib without any
changes.
|
|
|
|
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
|
|
|
|
Daniel Schepler.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
"simpl at" and "change at".
|
|
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
|
|
right-hand side of a "change with": the rhs lives in the toplevel
environment.
|
|
|
|
|
|
|
|
definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).
|
|
|
|
where it will eventually stabilize.
|
|
|
|
Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
|
|
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
|
|
normally, so failure is now detected by removing the "Fail".
|
|
|
|
|
|
intropattern or a bound ltac variable).
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
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).
|
|
|
