| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
| |
folded primitive projections in applicative stacks in rhs as named, hence
prefering to unfold the lhs in these cases.
|
| | |
|
| |
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
| |
|
|
| |
in cases of unification with existentials requiring it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
| |
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.
|
| | |
|
| |
|
|
|
| |
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
with existing ML code.
|
| |
|
|
| |
for e_contextually where it is used. Bug #3648 is fixed.
|
| |
|
|
| |
matching partial applications of primitive projections. Fixes bug #3637.
|
| | |
|
| |
|
|
| |
equality of universes, along with a few other functions in evd.
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| |
|
|
|
| |
was failing in this case due to the wrong postponment of an unsolvable
?X = RigidContext[?X] problem.
|
| |
|
|
| |
primitive projections.
|
| |
|
|
| |
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
| |
|
|
|
|
| |
compare bodies
of convertible types! Bug found by B. Ziliani.
|
| |
|
|
|
|
|
|
|
|
|
| |
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
| |
|
|
|
|
|
| |
pruning),
hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but
backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
|
| |
|
|
| |
of metas/evars
|
| |
|
|
|
| |
to match on a primitive projection application c.(p) using "?f _", binding f
to (fun x => x.(p)) with the correct typing.
|
| | |
|
| |
|
|
|
| |
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
|
| |
|
|
| |
its expansion if it could reduce (fixes bug #3480).
|
| | |
|
| |
|
|
|
| |
which made CoRN (and probably Ergo) fail. Another option should be found for
making a constant not unfoldable by tactics/refinement.
|
| |
|
|
|
|
| |
converting
the stacks. Take care of this by recalling unification.
|
| |
|
|
|
|
| |
cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
|
| |
|
|
|
|
|
| |
matching
infered predicate, instead of the arguments ts which might be empty (e.g. in unification).
Fixes failure in success/unification.v
|
| | |
|
| | |
|
| |
|
|
| |
- Remove dead code in evarconv.
|
| |
|
|
| |
primitive projections obey the Arguments command.
|
| |
|
|
|
|
|
|
| |
Universes.
Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
the merge).
Obligations are not necessarily opaque.
|
| | |
|
| |
|
|
|
| |
abstraction has the right type. Fixes bug# 3306.
Add test-suite files for bugs 3305 and 3306.
|
| |
|
|
|
| |
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
|
| |
|
|
|
|
|
|
| |
indeed unifies
with the projected term, keeping track of universes).
- Fix the [unify] tactic to fail properly.
- Fix unification to disallow lowering a global Type(i) universe to Prop or Set.
|
| |
|
|
|
|
|
|
|
| |
universes (better semantics
for axioms, opaque constants).
Conflicts:
pretyping/evarconv.ml
|
| |
|
|
|
|
| |
- Shortcut for Set <= x checks, assuming that this is always true except when
x (or rather its canonical representative) is Prop. Invariant to check.
- Uncomment the profiling code and make it depend on a (statically known) boolean.
|
Matthieu Sozeau
Hugo Herbelin
Arnaud Spiwack
Matthieu Sozeau
Pierre-Marie Pédrot