| Age | Commit message (Collapse) | Author |
|---|
|
equality of universes, along with a few other functions in evd.
|
|
apply f, g,... so that apply f, g. succeeds when apply f; apply g
does. It just mimicks the behavior of rewrite foo bar.
|
|
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).
|
|
All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).
|
|
identifiers.
Fixes Ergo.
|
|
|
|
non-dependent or propositional constraint has already been found
(same behavior as before previous patch).
|
|
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).
|
|
|
|
|
|
|
|
the abs flag in rewrite.
|
|
|
|
|
|
|
|
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
evars was too liberal. Using an intermediate criterion which makes
both tests apply.v and 3284.v working.
|
|
|
|
|
|
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).
|
|
compatibility with inversion
|
|
generated equation names).
|
|
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).
|
|
|
|
|
|
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.
|
|
|
|
|
|
Left a README, just in case someone will discover the remnants of it
decades from now.
|
|
|
|
- [induction] on inductive records use the generated induction scheme for induction (not destruct as for non-recursive records)
- [induction] on non-recursive variants do destruct as the induction scheme is not generated.
|
|
The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
|
|
[uconstr:(…)].
- The binders names can be influenced by binders defined in Ltac (e.g. [let x:=fresh"y" in let u:=constr:(fun x:nat=>x) in idtac u] ).
- Any untyped constr in the context can now be inserted and type-checked inside a constr. In particular, Gregory Malecha's original proposed syntax for type-checking untyped terms in Ltac is now available [let u:=uconstr:(I I) in let v := constr:(u) in idtac v].
|
|
|
|
that it clears things earlier in the "as" case, allowing
intros_replacing to work without renaming the hypotheses.
(clear_request was not a good idea here a priori, since its use was
not related to the hypothesis to invert but to an hypothesis to inject).
|
|
necessarily granting names given in the "as" clause.
|
|
|
|
|
|
|
|
|
|
Instead of passing glob tactics through the infamous globTacticIn hack and
antiquotation feature of the Ltac syntax, we put them in the interpretation
environment as closures. This should be used everywhere to get rid of this
buggy antiquotation syntax.
This fixes bug #2800.
|
|
|
|
|
|
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
|
Fixes bug #3455.
|
|
The refined term is still typechecked twice (not counting Qed). But there seem to be a bug in the typechecker whereby it sometimes return terms which have universe inconsistencies. Until this is fixed, I'll leave the second typing phase which seems to catch these inconsistencies. To remove it, it suffices to change the [unsafe] flag to [true].
|
|
|
