| Age | Commit message (Collapse) | Author |
|---|
|
for e_contextually where it is used. Bug #3648 is fixed.
|
|
and pretyping which was not contracting the eta-expanded forms in presence
of coercions.
|
|
|
|
|
|
projections in the term.
|
|
matching partial applications of primitive projections. Fixes bug #3637.
|
|
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
|
|
|
|
in Class_tactics).
|
|
|
|
|
|
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.
|
|
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.
|
