| Age | Commit message (Collapse) | Author |
|---|
|
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).
|
|
presence of let-ins.
|
|
|
|
|
|
All superscript numbers are now symbols instead of parts of identifiers.
This disallows some identifiers, but hopefully not a lot of people were
using superscripts as part of identifiers, weren't they?
|
|
behavior of evar_conv_x,
getting more common after patch on evars and eta. The main problem is that ?X = C[?X] problems get
postponed now, when they failed earlier before (rendering the algorithm incomplete, e.g. on ?X = \y. ?X y).
A notion of "rigid/strongly rigid" occurrences would give a better fix.
|
|
Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.
|
|
Coq now accepts the [Universes u1 ... un] syntax.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
For consistency with ChoiceFacts
|
|
The generalized versions are names *_one_var. We preserve backwards
compatibility by defining the old versions in terms of the generalized
ones.
This closes the rest of Bug 3019, and closes pull request #6.
|
|
stm test-suite files.
|
|
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.
|
|
|
|
cases pattern variables than for naming forall/fun binders (but still
avoiding constructor names).
Note in passing: such as it is implemented, the general strategy is in
O(n²) in the number of nested binders, because, when computing the
name for each 'fun x => c" (or forall, or a pattern name), the names
from the outside c and visibly occurring in c are computed.
|
|
Should we also add is_* tactics for other things? is_rel, is_meta,
is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const,
is_ind, is_constructor, is_case, is_proj?
|
|
|
