| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).
|
|
|
|
|
|
|
|
|
|
Stop sharing those references across constants of the same
module, which was triggering some bugs when using native_compute
in interactive mode in a functor declaration.
|
|
matching subterm destruct/induction on a partially applied
pattern. AFAICS, there is only such instance of destruct that needs
this in the contrins (in EuclideanGeometry/G3_ParticularAngle.v), but
while a more global decision is taken, I prefer at the current time to
adopt this approximation of 8.4 semantics, even if the flags are not
the same when the pattern is fully applied or not. Only so little
cases are concerned because in most cases, destruct/induction on a
partially applied pattern is of the form "destruct cst"
(e.g. "destruct eq_dec") and no conversion is needed anyway.
Not being uniform whether the pattern is fully applied or not is a bit
unsatisfactory, but hopefully, this is temporary.
|
|
where it will eventually stabilize.
|
|
|
|
|
|
absence of remaining dependent evars when several arguments are given.
For simplicity of implementation, checking instead for every step of
the n-ary "apply in".
|
|
This is a continuation of the previous patch.
|
|
As witnessed in the ProjectiveGeometry contrib, some evar normalization were
taking ages because of an exponential behaviour due to a call-by-name
substitution: when normalizing an evar, its arguments were substituted right
away and the resulting term was then normalized, leading to a potential
duplication of normalizations.
Now we normalize evar arguments before substituting them, in a call-by-value
fashion. It makes examples from ProjectiveGeometry compile instanteanously
when they were killing the machine due to excessive memory allocation before
the patch.
Note that there is a tension here: we may be normalizing evar arguments too
eagerly, and try a call-by-need approach instead. To choose which particular
strategy we use, we should do some benchmarks... On stdlib, call-by-value
and call-by-need seem indistinguishable. To be continued?
|
|
I'm afraid this fix is a bit heuristic, but it seems to generate correct code in
all cases.
|
|
|
|
|
|
|
|
|
|
|
|
The Info layer was setting the required evarmap too eagerly, making the
tclWITHHOLE tactical accept terms with holes. The logging facility is
now inside the tclWITHHOLES.
|
|
|
|
|
|
|
|
Pretyping of [if] cases was missing a convertibility check with the ambient
type constraint, and just dropped it. This was making the pretyper construct
ill-typed terms.
|
|
- drops all Defined entries from the evar map (applying the subst to the
initial evar and the undefined evars types).
- call Gc.compact
Now the question is: where should these two commands be documented?
|
|
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).
|
|
One missing evar was making the whole substitution fail.
The bug actually existed a priori also in the case where only metas
are substituted (i.e. before bcba6d1bc9f769da), leading to limit the
number of situations where it could be effectful.
This fixes current failures of RelationAlgebra and CFGV.
|
|
- Do use the flag for_ml for distinguishing coq level and ml level
ltac definitions.
- Skip ML call from the trace.
There are still differences from 8.4 and trunk. For instance on:
Ltac f x := refine x.
Goal False.
f I.
8.4 says:
In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed.
Error: The term "I" has type "True" while it is expected to have type "False".
trunk says:
In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed.
Error: The term "I" has type "True" while it is expected to have type "False".
Maybe we would like a mix of both (besides the printing of a
non-elegant "<genarg:uconstr>)?
|
|
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
|
|
normally, so failure is now detected by removing the "Fail".
|
|
|
|
|
|
for Functional Induction was failing because of minus now an alias).
Knowing that minus is an alias for Sub.nat, there are still two bugs in
Functional Induction (Pierre or Julien?):
"Functional Scheme minus_ind := Induction for minus Sort Prop." is
failing when Nat is not imported.
"functional induction (minus n m)" is failing because looking for
sub_ind while the scheme is named minus_ind.
|
|
functional induction).
|
|
|
|
intropattern or a bound ltac variable).
|
|
|
|
|
|
|
|
Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad).
|
|
|
|
|
|
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.
|
|
|
|
|
