| Age | Commit message (Collapse) | Author |
|---|
|
scope" error message).
|
|
it became possible to have binding names themselves bound to ltac
variables (2fcc458af16b).
|
|
glob_constr to constr_pattern. Was partially fixed to solve #3088
(8e88b7adab) in but the order of lambdas was still incorrect as the
fix of the order of lambdas in second-order pattern-matching for #3136
showed (83159124ce22).
|
|
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.
|
|
|
|
|
|
|
|
by names): VarInstance behaves like GoalEvar for type class
resolution.
|
|
reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f:
using renaming also in retyping.
|
|
(the action is "clear").
Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.
Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
|
|
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
|
using whd_state_gen to handle unfolding. Add an isProj/destProj
in term. Use the proper environment everywhere in unification.ml.
|
|
- Removed collect_evars which does not consider instance
(use evars_of_term instead).
- Also removed evars_of_evar_info which did not filter context (use
evars_of_filterered_evar_info instead). This is consistent with
printing goal contexts in the filtered way.
Anyway, as of today, afaics goals filters are trivial
because (if I interpret evarutil.ml correctly), evars with
non-trivial filter necessarily occur in a conv pb. Conversely,
conv pbs being solved when tactics are called, there should not be
an evar used as a goal with a non-trivial filter.
|
|
unification for apply (compatibility reason). Waiting for another way
to provide a more uniform scheme by default (keyed unification?).
|
|
their eta-expanded forms which can then unfold back to the unfolded
primitive projection form. This removes all special code that
was necessary to handle primitive projections before, while keeping
compatibility.
Also fix cbn which was not refolding primitive projections correctly
in all cases.
Update some test-suite files accordingly.
|
|
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
|
|
|
|
|
|
|
avoid looping and be compatible with unfold.
|
|
|
|
|
|
for primitive projections, fixing bug #3661. Also fix expand_projection
so that it does enough reduction to find the inductive type of its
argument.
|
|
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
|
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
|
|
|
|
with existing ML code.
|
|
|
|
projections with their eta-expanded constant form.
|
|
Maintain the user-level view of primitive projections,
disallow manual unfolding and do not let hnf give the eta-expanded
form.
|
|
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).
|
|
|
