| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
|
|
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.
|
|
|
|
|
|
for typeclass errors.
|
|
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
|
|
its expansion if it could reduce (fixes bug #3480).
|
|
applications, solving part of bug #3503.
|
|
|
|
|
|
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
|
|
The levels added by the context are in general much fewer than the size of the
evarmap, so it is better to add them to the latter rather than doing it the
other way around.
|
|
|
|
|
|
This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine.
As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
|
|
|
|
obtained from case analysis or induction. Made it under experimental status.
This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was
acting at the level of logic.ml. Now acting in tactics.ml.
Parts of things to be done about naming (not related to Propositions):
induction on H:nat+bool produces hypotheses n and b but destruct on H
produces a and b. This is because induction takes the dependent scheme
whose names are statically inferred to be a and b while destruct
dynamically builds a new scheme.
|
|
- Decomment code in reductionops forgotten after debugging.
|
|
variables.
Simplifies instantiation of constants/inductives, requiring less allocation and Map.find's.
Abstraction by variables is handled mostly inside the kernel but could be moved outside.
|
|
- Allow apply's unification to use conversion even if some polymorphic
constants appear in the goal (consistent with occur_meta_or_evar, and
evarconv in general).
|
|
|
|
- realargs: refers either to the indices of an inductive, or to the proper args
of a constructor
- params: refers to parameters (which are common to inductive and constructors)
- allargs = params + realargs
- realdecls: refers to the defining context of indices or proper args
of a constructor (it includes letins)
- paramdecls: refers to the defining context of params (it includes letins)
- alldecls = paramdecls + realdecls
|
|
catched otherwise due to the discrepancy between evars and metas.
|
|
|
|
Specifications indicating that the record object must be a constructor. Fixes bug #3432.
|
|
|
|
unification, speeding it up considerably
Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410
|
|
which
results in strange changes in user provided terms.
|
|
|
|
|
|
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.
|
|
from MathClasses).
|
|
kernel in library/universes.ml.
|
|
cleanly when called
on partially applied constructors. Also protect evar_conv from that case.
|
|
of the universe context in the obligations, it gets gradually fixed
globally by each one of them.
Fixes bug found in Misc/Overloading.
|
|
invariant that the evar arguments to that function always have to be undefined.
|
