| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
of resulution for goals whose head is "ref". + means the argument
is an input and shouldn't contain an evar, otherwise resolution
fails. This generalizes the Typeclasses Strict Resolution option
which prevents resolution to fire on underconstrained typeclass
constraints, now the criterion can be applied to specific parameters.
Also cleanup auto/eauto code, uncovering a potential backwards
compatibility issue: in cases the goal contains existentials, we
never use the discrimination net in auto/eauto. We should try to
set this on once the contribs are stabilized (the stdlib goes through
when the dnet is used in these cases).
|
| |
|
|
|
| |
substitution at the right place.
I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
|
| |
|
| |
The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
|
| |
|
|
| |
records in unification.ml.
|
| | |
|
| |
|
|
|
|
|
| |
Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
in instances.
|
| |
|
|
| |
was working in 8.4.
|
| | |
|
| | |
|
| |
|
|
|
| |
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
| |
|
|
|
|
|
| |
matching (i.e. no instanciation of the goal evars).
Classes defined when [Set Typeclasses Strict Resolution] is on
use the restricted resolution for all their instances (except
for Hint Extern's).
|
| |
|
|
|
| |
was failing in this case due to the wrong postponment of an unsolvable
?X = RigidContext[?X] problem.
|
| | |
|
| |
|
|
|
|
|
| |
When w_unifying primitive projection applications, force
the unification of types of the projected records to recover instances
for the parameters (evarconv does this automatically by unifying evar
instances with their expected type).
|
| |
|
|
|
|
|
|
|
|
| |
selection (rewrite, destruct/induction, set or apply on scheme), for
unification (apply on not a scheme, auto), the latter being separated
into primary unification and unification for merging instances.
No change of semantics from within Coq, if I did not mistake (but a
function like secondOrderAbstraction does not set flags by itself
anymore).
|
| |
|
|
| |
Let r.(p) be a strict subterm of r during the guardness check.
|
| |
|
|
|
|
|
|
| |
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
|
| | |
|
| |
|
|
| |
primitive projections.
|
| |
|
|
| |
use of projections.
|
| | |
|
| |
|
|
| |
context for goal contexts.
|
| |
|
| |
Binder names are interpreted as the Ltac specified one if available.
|
| |
|
|
|
|
|
|
|
| |
In order not to be too costly, there is an [unsafe] flag to be set if the
tactic does not have to check that the partial proof term is well-typed (to
be used with caution though).
This patch breaks one [fix]-based example in the refine test-suite, but a huge
development like CompCert still goes through.
|
| | |
|
| | |
|
| |
|
|
|
| |
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
|
| |
|
|
| |
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.
|
| | |
|
| |
|
|
|
| |
and their eta-expanded forms succeed, potentially filling parameter
metavariables from the type information of the projected object.
|
| |
|
|
| |
Second-order pattern-matching now respect variable abstraction order.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
Matthieu Sozeau
Arnaud Spiwack
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
Pierre Boutillier
Jason Gross