| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
now fails with Error: Already an existential evar of name Main
|
| |
|
|
|
|
|
|
| |
forms in evarconv and unification, as well as fallback to first-order
unification when eta for constructors fail. Update test-suite file
3484 to test for the FO case in evarconv as well.
|
|
|
|
| |
of the record binder for Class C's projections.
|
|
|
|
|
| |
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
|
|
|
|
| |
unification.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
2nd-order matching).
We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is
well-typed when taking the filtered context Gamma) in 2nd order
matching. Maybe this weakens the power of the 2nd order matching
algorithm, so it is not clear that it is the good fix.
Another fix could have been to ensure that taking the closure of
filter does not extend it beyond the original filter (hence keeping
the filter untyped if it was already untyped).
As for the bug #3045, it also revealed that some "destruct c as [[]]"
could be made stronger as decomposing the destruct in two parts
"destruct c as [x]; destruct x" workis while it currently fails if in
one part.
|
| |
|
| |
|
|
|
|
| |
condition.
|
|
|
|
|
| |
type, what is necessary condition to ensure that the conversion of
bodies will not raise an anomaly).
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
inductives).
The implementation constant should have the a universe instance
of the same length, we assume the universes are in the same order
and we check that the definition does not add any constraints
to the expected ones. This fixes bug #3670.
|
| |
|
|
|
|
|
| |
Naming a Ltac definition like a built-in tactic used to fail, but now only
spits out a warning. This is too complicated to test...
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
| |
3566 gave a legitimate error, keyedrewrite was not setting keyed
unification on.
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
| |
avoid looping and be compatible with unfold.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
Maintain the user-level view of primitive projections,
disallow manual unfolding and do not let hnf give the eta-expanded
form.
|
|
|
|
| |
for e_contextually where it is used. Bug #3648 is fixed.
|
|
|
|
| |
matching partial applications of primitive projections. Fixes bug #3637.
|
|
|
|
|
|
|
| |
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
|
|
|
|
| |
equality of universes, along with a few other functions in evd.
|
|
|
|
|
| |
apply f, g,... so that apply f, g. succeeds when apply f; apply g
does. It just mimicks the behavior of rewrite foo bar.
|
|
|
|
|
|
|
|
| |
appear in the"
This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8.
Not the right way to do it. The evd shouldn't contain unrelated evars in the first place.
|
|
|
|
|
| |
clenv's value and type, ensuring we don't try to solve unrelated
goals (fixes bug#3633).
|
|
|
|
| |
examples.
|