| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.
This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.
Another part is still open (see test-suite).
|
| |
|
|
|
|
|
|
|
|
|
| |
but the internal representation dropped let-in.
Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.
To do, there is still an extra @ in the constructor name that does not
need to be there.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc).
It may be the case that the new expression lives in a higher sorts and
the context where it is substituted in supports it. So, it is too
strong to expect that, when the substituted objects are types, the
sort of the new one is smaller than the sort of the original
one. Consider e.g.
Goal @eq Type nat nat.
change nat with (@id Type nat).
which is a correct replacement, even if (id Type nat) is in a higher sort.
Introducing typing in "contextually" would be a big change for a
little numbers of uses, so we instead (hackily) recheck the whole term
(even though typing with evars uses evar_conv which accept to unify
Type with Set, leading to wrongly accept "Goal @eq Set nat nat.
change nat with (@id Type nat).". Evar conv is however rejecting
Prop=Type.)
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
projections in cbv when delta _and_ beta flags are set. Add test-suite
file for bug 3700 too.
|
| |
|
|
|
| |
Fix typeclass resolution which was considering as subgoals
of a tactic application unrelated pre-existing undefined evars.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
- Optimize the removal of generalization when there is no dependency in
the generalized variable (see postprocess_dependencies, and the removal
of dependencies in the default type of impossible cases).
- Compute the onlydflt flag correctly (what allows automatic treatment
of impossible cases even when there is no clause at all).
|
| | |
|
| | |
|
| |
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
- unbound variables in notation are allowed, forcing only parsing mode
- plus and mult are now themselves abbreviations
- evars are named
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This reverts commit cc06ffe3df0ecc023ad046a085b0751ed4161cbf.
Going back to the convention of naming bound variables in hypotheses
of the goal as in 8.4.
My arguments for the revert are:
- apply ... with (id:=...) would have to be changed too, then possibly
breaking the compatibility
- the naming became dependent of the order of variables as in
x:nat
H:forall x0, x0=0
=====
goal
but
H:forall x, x=0
x:nat
=====
goal
Accordingly, this is all a matter of convention, since the meaning of
bindings is anyway the same in both cases.
|
| |
|
|
|
| |
constants which without a @ would have a maximally inserted implicit
argument.
|
| | |
|
| |
|
|
|
| |
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...
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
(the action is "clear").
Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.
Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
|
| |
|
|
|
| |
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
|
| | |
|
| | |
|
| |
|
|
|
| |
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.
|
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
Matthieu Sozeau
Xavier Clerc