| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
| |
Just like the [Record] keyword allows only non-recursive records.
|
| | |
|
| | |
|
| |
|
|
|
| |
and their eta-expanded forms succeed, potentially filling parameter
metavariables from the type information of the projected object.
|
| |
|
|
|
| |
This should allow tactics after a Goal.enter not to have to renormalize
them uselessly.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
|
| | |
|
| | |
|
| |
|
|
|
| |
The comparison on terms which triggers new printing flags in case two terms which are different would be printed identically now contains α-equivalence.
The implementation using a canonization function on [constr] instead of trying to deal with [constr_expr] was suggested by Hugo.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Parametric printers are now using a record to ease the error reporting when
modificating code. Further improvement may include the use of the object
layer of OCaml, which would fit in this particular context.
|
| | |
|
| |
|
|
| |
Second-order pattern-matching now respect variable abstraction order.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
fresh names interferring with names later generated in intropatterns
(as introduced in 72498d6d68ac which passed "clenv_refine_in continued
by pattern introduction" to descend_in_conjunction while only a pure
clenv_refine was passed before). The 72498d6d68ac version was
generating fresh names in the wrong order (morally-private names for
descend_in_conjunction before user-level names in clenv_refine_in).
The 19a7a5789c fix was introducing expressions not handled by the
refine from logic.ml.
In particular, this fixes RelationAlgebra.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
It was actually useless, because its only use was in the moved away
decompose tactic.
|
| | |
|
| |
|
|
|
|
| |
compare bodies
of convertible types! Bug found by B. Ziliani.
|
| |
|
|
|
| |
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
|
| | |
|
| |
|
|
|
|
| |
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
|
| |
|
|
|
| |
This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.
|
| |
|
|
|
|
|
|
|
|
|
| |
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
| | |
|
| |
|
|
|
| |
Instead of having a version of unpackers for each level, we use a dummy argument
to force unification of types.
|
| |
|
|
|
|
| |
at least remove the successes obtained by trivial unification of a
meta with the goal, so as to avoid surprising results. We generalize
this to variables which will only eventually be replaced by metas.
|
| |
|
|
|
| |
Indeed, generalized binders are unnamed, because their name is generated on the
fly.
|
| |
|
|
| |
eta-expanded version of a projection as before.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
The unification oracle now prefers unfolding the eta-expanded form of a
projection over the primitive projection, and allows first-order
unification on applications of constructors of primitive records,
in case eta-conversion fails (disabled by previous patch on eta).
|
| |
|
|
|
|
|
| |
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).
|
Arnaud Spiwack
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Pierre Boutillier
Enrico Tassi
Pierre Boutillier