| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
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).
|
| |
|
|
|
| |
hypothesis when indices also occur among parameters.
This solves current failure of PersistentUnionFind.
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
| |
This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
|
| |
|
|
|
| |
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).
|
| | |
|
| |
|
|
| |
occurrences: some uniformisation was not appropriate for "change").
|
| |
|
|
| |
[Info] command.
|
| |
|
|
|
|
| |
Some particular care needed to be taken to print aliases properly.
The printing of argument is just the generic printer for [genarg]. The trouble is that (apart from being incomplete), it does not know that it's printing Ltac arguments. As a consequence, the arguments are not properly quoted (e.g. if they are tactic expressions, they are not within [ltac:(...)].
|
| |
|
|
| |
Empirically it works better on some notations than on others and I have no idea why. I've seen notations not printing their arguments, for instance, and other printing perfectly.
|
| |
|
|
| |
Since PMP's intervention, the [TACTIC EXTEND] tactics are not uniform: some are syntax, and some are just an internal name for an Ltac definition. The latter kind prints an internal name. It may be better to avoid printing them in the trace altogether. But I haven't figured out how to detect that properly yet.
|
| |
|
|
|
|
|
|
| |
The printing uses the printer for interpreted tactics. It only works for tactics which are defined in the new style. There are still a few atomic tactics in tacinterp which are defined in [V82] style. Namely:
exact, apply, clear, rename, reduce, change, (mutual variant of) fix, (mutual variant of) cofix
These print placeholder names which are never reparsable and not as useful.
|
| | |
|
| |
|
|
|
|
| |
clause; extended it so that an induction over "x" is considered
generic when the clause has the form "in H |-" (w/o the conclusion)
and x does not occur in the conclusion.
|
| |
|
|
|
|
|
| |
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".
|
| | |
|
Pierre-Marie Pédrot
Arnaud Spiwack
Hugo Herbelin
Enrico Tassi