| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
| |
on vm and #3068 by Nov 2 commit on destruct.
Also fixed test for failure of #3459.
|
| |
|
| |
|
| |
|
|
|
|
|
| |
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
|
|
|
|
|
|
|
| |
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
examples.
|
|
|
|
|
|
|
|
| |
contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.
|
| |
|
| |
|
|
|
|
|
| |
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
|
| |
|
| |
|
| |
|
|
|
|
|
| |
is has non-local effects. For now it is not disabled by default, but we'll
try to disable it once the test-suite and contribs are stabilized.
|
|\
| |
| |
| | |
JasonGross-tc
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
the hypotheses in eauto.
|
| | |
|
| | |
|
| | |
|
|\ \
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
JasonGross-more-test-suite
Conflicts:
test-suite/bugs/closed/3300.v
test-suite/bugs/closed/3373.v
|
| | | |
|
| | | |
|
| | | |
|
| |/
|/| |
|
| |
| |
| |
| | |
Every time you use abstract a kitten dies, please stop.
|
|/ |
|
|
|
|
|
| |
there is not the same as in Evd.define.
- Fixed bugs #3330 and #3331.
|
| |
|
|
|
|
| |
equation, fix uncaught exception in setoid_rewrite (bug #3336).
|
|
|
|
| |
Fixes bug #3346.
|