| Age | Commit message (Collapse) | Author |
|---|
|
|
|
As their commit messages suggested it, these commits were not intended
to be committed at this time. They are part of a on-going merge of the
code of induction and functional induction. Together with the fix
here, they are supposingly transparent, semantically speaking.
|
|
[Proofview].
The primitives in [Tacticals] respect Ltac's error level, whereas the one in [Proofview] do not necessarily. In that case the error caught was ignored causing arbitrary error level after [constructor] to be canceled.
Needed the addition of an [ORD] variant to [OR] in [Tacticals.New] to avoid unnecessary precomputation (the 'D' stands for 'delay').
Fixes #3838.
|
|
|
|
|
|
|
|
|
|
propagate it. This allows C-zar to continue to work.
Don't know if it is the best way to do it.
|
|
normalize it afterwards.
|
|
In particular, the old hypinfo is made as a proper cache, preventing dynamic
tricks to decide whether it was rightful to refresh it.
|
|
env.
|
|
This allows to have the example in test setoid_unif.v to work again.
|
|
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
|
in tactic unification.
|
|
|
|
at least when f is an evaluable reference.
|
|
when the arguments of a constructor can be moved at the place of the
variable on which destruct or induction applies.
|
|
a UserError to ease debugging.
|
|
|
|
- removed the encapsulation in a Tactic Failure (I don't see why
setoid_rewrite should specifically raise a Fail - do I miss something?)
- avoid having twice a "Unable to satisfy ... constraints" message.
|
|
|
|
|
|
quantified hypothesis in functional induction. This has apparently no
visible effect, probably because functional schemes do not have
non-dependent hypothesis in their branches besides induction
hypotheses which are anyway introduced at the top of the context.
|
|
|
|
anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
|
|
of the function are dependent.
|
|
|
|
|
|
|
|
|
|
|
|
Before this patch, when tactics-in-terms were relying on the ugly environment-
modifying primitives such as tclABSTRACT, the returned term was ill-typed
because the resulting effects were just dropped. Now we modify the returned
term on the fly, effectively getting rid of the effects it may depend on.
Yet, this is not completely satisfactory, because the tactic may solve some
goals at distance (I would have said by side-effect, but this is ambiguous
here). If ever the resulting terms are depending on the side-effects of the
tactic, then we are still unsound.
This patch should handle most of the use-cases gracefully. To really solve this
issue, we should rewrite the pretyper in the new monad, which is easier said
than done.
|
|
by commit bf0185694.
|
|
|
|
|
|
|
|
|
|
semantics described in the reference manual (i.e. if "f" is a qualid,
do not add implicit arguments and, a fortiori, do not try to solve
these implicit arguments - in particular, changing DbLib which
expected this rule not to be followed).
|
|
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).
|
|
|
|
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".
|
|
|
|
|
|
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.
|
|
|
|
|
|
- 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).
|
