| Age | Commit message (Collapse) | Author |
|---|
|
We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
the general sigma of the goal so that tactics have no such low-level
tclEVARS, Evd.merge, or check_evars to do:
- what takes tclEVARS and check_evars in charge is now a new
tactical of name tclWITHHOLES (this tactical has a flag to support
tactics in either the "e"- mode and the non "e"- mode);
- the merge of goal evars and holes is now done generically at
interpretation time (in tacinterp) and as a side-effect it also
anticipates the possibility to refer to evars of the goal in the
arguments;
- with this approach, we don't need such constr/open_constr or
bindings/ebindings variants and we can get rid of all ugly
inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
this is the case e.g. of "rewrite !c" which morally reevaluates c at
each new rewriting step; this kind of tactics still receive a
specific sigma around their arguments and they have to merge evars
and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
instantiated in tactics (here apply and apply in) that should not open
existential goals (see Bas Spitters' coq-club mail about "exists" leaving
open existentials).
- Preserved the history of the evars occurring in bindings.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12345 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
agreement with wish #2117 (pattern unification of evars remained
deactivated for 3 years because of incompatibilities with eauto [see
commit 9234]; thanks to unification flags, it can be activated for
apply w/o changing eauto).
Also add test for bug #2123 (see commit 12228).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
traînaient un peu partout dans le code depuis la fusion d'evar_map et
evar_defs. Début du travail d'uniformisation des noms donnés aux
evar_defs à travers le code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
major changes in [w_unify] and the conversion functions used by it to
handle the sort constraints correctly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
universes as usual, we add the new universes to the sort constraints and
do unification modulo those ([constr_unify_with_sorts]): this allows to
instanciate Type i with Prop for example and keep track of it. The sort
constraints are thrown away at the end of unification for the moment,
but we can detect inconsistencies during unification.
Make unification more symmetric as well w.r.t. substitution of defined
metas.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12137 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Primitive setup for firing typeclass resolution on-demand: add a flag to
control resolution of remaining evars (e.g. typeclasses) during
unification.
- Prevent canonical projection resolution when no delta is allowed
during unification (fixes incompatibility found in ssreflect).
- Correctly check types when the head is an evar _or_ a meta in w_unify.
Move [isEvar_or_Meta] to kernel/term.ml, it's used in two places now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12131 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the interpretation mechanism of ltac variables)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par Evd). Ça s'accompagne de quelques autres modifications de
l'interface (certaines fonctions étaient des doublons, ou des
conversions entre evar_map et evar_defs).
J'ai modifié un peu la structure de evd.ml aussi, pour éviter des
fonctions redéfinies deux fois (i.e. définies trois fois !), j'ai
introduit des sous-modules pour les différentes couches.
Il y a à l'heure actuelle une pénalité en performance assez sévère (due
principalement à la nouvelle mouture de Evd.merge, si mon diagnostique
est correct). Mais fera l'objet de plusieurs optimisations dans les
commits à venir.
Un peu plus ennuyeux, la test-suite du mode déclaratif ne passe plus. Un
appel de Decl_proof_instr.mark_as_done visiblement, je suis pour
l'instant incapable de comprendre ce qui cause cette erreur. J'espère
qu'on pourra le déterminer rapidement.
Ce commit est le tout premier commit dans le trunk en rapport avec les
évolution futures de la machine de preuve, en vue en particulier
d'obtenir un "vrai refine".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
right unification flags for exact hints in eauto (may break a lot of
things by succeeding much more often).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
s'est avéré ralentir la compilation des user-contribs au final, sans
compter aussi le bug 1980 apparemment introduit par ce commit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
avoid trying to resolve classes early in open constr arguments for Ltac,
the tactics themselves should do whatever's appropriate with the constraints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11503 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
type contains a meta as this is currently unsupported in the
refiner. Fixes bugs #1980 and #1981.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
abusivement sur les clauses.
Nettoyage au passage de metamap qui était utilisé à la fois pour les
substitutions de meta et pour les contextes de typage de meta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
discriminate/injection/simplify_eq acceptent maintenant un terme
comme argument. Les clauses "with" et les variantes "e" sont aussi
acceptées. Aussi, discriminate sans argument essaie maintenant
toutes les hyps quantifiées (au lieu de traiter seulement les buts
t1<>t2).
--This line, and those below, will be ignored--
M doc/refman/RefMan-tac.tex
M CHANGES
M pretyping/evd.ml
M pretyping/termops.ml
M pretyping/termops.mli
M pretyping/clenv.ml
M tactics/extratactics.ml4
M tactics/inv.ml
M tactics/equality.ml
M tactics/tactics.mli
M tactics/equality.mli
M tactics/tacticals.ml
M tactics/eqdecide.ml4
M tactics/tacinterp.ml
M tactics/tactics.ml
M tactics/extratactics.mli
M toplevel/auto_ind_decl.ml
M contrib/funind/invfun.ml
M test-suite/success/Discriminate.v
M test-suite/success/Injection.v
M proofs/clenvtac.mli
M proofs/clenvtac.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
des types des with-bindings dans la 8.1 [ceux-ci étaient déjà
utilisés et ce qui est vraiment nouveau est que l'unification est
maintenant celle de evarconv alors que c'était avant un mélange
d'unify_0 (sans delta) et de coercion sur les termes sans evars]. Je
renonce à maintenir la compatibilité (on se retrouve donc avec un
exemple qui fonctionne différement dans TermsConv.v de CoLoR).
- Robustesse accrue pour la nouvelle facilité de syntaxe de binding
avec paramètre pour pose/set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10856 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"pose as" de Program.
- Report des modifs de coercion.ml (révision 10840) dans subtac_coercion.ml.
- Comportement de "simple apply" rendu plus proche de celui du apply 8.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10854 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
term unification (for constant and variable delta unfolding) and one to
parameterize closed-term conversion. Most of the time conversion uses
full delta and unification does no delta. This fine-grain is used in
rewrite/setoid_rewrite, where only closed-term delta on global constants
is allowed.
- Interpret Hint Unfold as a directive for delta conversion in
auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints).
- Remove ad-hoc support for this in typeclasses. Now setoid_rewrite
works correctly w.r.t. the old version regarding local definitions.
- Fix closed bugs which needed updating due to syntax modifications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to
setoids. Add corresponding test files.
- Add new modulo_zeta flag to control zeta during unification (e.g. not
allowed for setoid_rewrite unification, but ok for almost everything
else).
- Various fixes in class_tactics with respect to evars and error
messages.
- Correct error message for NoOccurenceFound, distinguishing between a
rewrite in the goal or an hypothesis.
- Move notations for ==>, --> and ++> to level 90 as suggested by
Russell O'Conor.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10813 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- vérification de la cohérence des ident pour éviter une option -R
avec des noms non parsables (la vérification est faite dans
id_of_string ce qui est très exigeant; faudrait-il une solution plus
souple ?)
- correction message d'erreur inapproprié dans le apply qui descend dans les
conjonctions
- nettoyage autour de l'échec en présence de métas dans le prim_refiner
- nouveau message d'erreur quand des variables ne peuvent être instanciées
- quelques simplifications et davantage de robustesse dans inversion
- factorisation du code de constructor and co avec celui de econstructor and co
Documentation des tactiques
- edestruct/einduction/ecase/eelim et nouveautés apply
- nouvelle sémantique des intropatterns disjonctifs et documentation des
pattern -> et <-
- relecture de certaines parties du chapitre tactique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
setoid rewrite. Refine and use the new unification flags setup by Hugo
to do a little bit of delta in clenv_unify/w_unify. Moved from a boolean
indicating conversion is wanted to a Cpred representing the
constants one wants to get unfolded to have more precise control. Add
corresponding test-suite file.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10684 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Pour éviter de pénaliser auto, eauto, autorewrite, mise en place
d'une option "modulo_conv" pour contrôler l'usage de cette delta.
- Pour éviter que rewrite ne réussise trop souvent, la delta est
désactivée pour les tactiques d'élimination (une étude fine reste à faire).
- On n'utilise aussi delta que sur les sous-termes du problème
d'unification initial. C'est une heuristique qui est intuitive mais qui
reste à être évaluée.
- Au bilan, le surcoût en temps de compilation des theories est d'un
peu moins d'1%.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10557 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ajout de l'option with à (e)destruct et (e)induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10169 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(cas d'un terme sans Rel libre), introduction au passage d'un nouveau
type d'evar EvarGoal pour raffinement du message d'erreur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
de résoudre des buts comme celui-ci :
Record nat_retract : Type :=
{f1 : nat -> nat; f2 : nat -> nat; f1_o_f2 : forall x, f1 (f2 x) = x}.
Goal nat_retract.
exists (fun x => x) (fun x => x).
- Nouvelle tentative d'utilisation des types des metas/evars pour
inférer de nouvelles instances de metas/evars; permet par exemple
d'utiliser f_equal sans option with, mais aussi, avec la modif
précédente, de résoudre des buts tels que
Goal exists f:bool->Prop, f true = True.
exists (fun x => True).
[Les expériences passées avaient montré qu'en prenant en compte les
types dans l'unification, on peut unifier trop tôt une evars à une
mauvaise sorte; à défaut de mécanisme de prise en compte des problème
d'unification avec sous-typage, on s'est interdit ici d'unifier des
types qui sont des arités.]
- Tout les constr de tactic_expr deviennent des open_constr (même si seul
with_bindings les accepte au final... c'est pas l'idéal).
- Renommage env -> evd et templenv -> env dans clausenv.
- Renommage closed_generic_argument -> typed_generic_argument.
- Renommage closed_abstract_argument_type -> typed_abstract_argument_type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9842 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
be explicitely given, and ALL parameters and args of the scheme must
be given (only branches must be omitted). For the moment, only
principle like generated by GenFixpoint (functional induction) are
usable. That is the predicate must have a additional paramter like in:
(P x1 ... xn (f p1...pm x1...xn))
Example of use : induction x y (add x y) using add_ind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
