| Age | Commit message (Collapse) | Author |
|---|
|
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
|
product in setoid_rewrite.
Backport of d670c6b6ce from trunk.
|
|
regression on apply.
|
|
The interpretation of arguments of tactic notations were normalizing the goal
beforehand, which incurred an important time penalty. We now do this argumentwise
which allows to save time in frequent cases, notably tactic arguments.
|
|
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
|
|
Checking that a term was indeed a relation was made too early, as the
decomposition function recognized relations of the form "f (g .. (h x y))
with f, g unary and only h binary. We postpone this check to the very end.
|
|
unification.
|
|
reflexivity/symmetry/transitivity only need
RelationClasses to be loaded.
|
|
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
|
|
The performance enhancement introduced by a895b2c0 for non-polymorphic hints
was actually causing a huge regression in the polymorphic case (and was marked
as such). We fix this by only substituting the metas from the evarmap instead
of the whole evarmap.
|
|
|
|
Fixpoint/Definition.
|
|
|
|
|
|
[rewrite] was calling find_suterm using the wrong unification flags, not
allowing full delta in unification of terms with the right keys as desired.
|
|
|
|
Also ensure we stay compatible with 8.4: progress could now be made
simply because of beta redexes in the goal.
|
|
|
|
|
|
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
|
|
|
|
|
|
|
be cleared.
This should fix the contrib failures on tactics like "destruct (0)".
|
|
Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2].
|
|
This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.
|
|
|
|
on applications of inverse (flip) on a crelation.
This was poluting universe constraints of lemmas using generalized
rewriting in Type.
|
|
|
|
|
|
|
|
|
|
The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.
Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
|
|
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
|
|
|
Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.
|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
|
|
|
|
|
|
|
|
For pose/set/clearbody, I think it is clear that we want to preserve
the name and this commit do it.
For revert, I first did not preserve the name, then considered in
2ba2ca96be88 that it was better to preserve it.
For intro, like for revert actually, I did not preserve the name,
based on the idea that the type was changing (*). For instance if we have
?f:nat->nat, do we really want to keep the name f in ?f:nat after an
intro.
For revert, I changed my mind based on the idea that if we had a
better control of the name if we keep the name that if the system
invents a new one based on the type. I think this is more reasonable
than (*), so this commit preserves the name for intro.
For generalize, it is still not done because of generalize being in
the old proof engine.
|
|
Syntactic analysis of dependencies when atomizing arguments in destruct
was not dealing properly with primitive projections hiding their
parameters.
|
|
inconsistent).
|
|
is buggy in general.
|
|
|
|
|
|
It is too bad that OCaml does not warn when catching an exception over a
closure rather than inside it.
|
|
presence of hints modifying the context and of a "using" clause.
Incidentally opening Hints by default in debugger.
|
|
Keep user-side information on the names used in instances of universe
polymorphic references and use them for printing.
|
