aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2002-12-24code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3481 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-23Re-essai de forcer le terme réécrit à apparaître dans le butherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3480 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationherbelin
faite par Rewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19suite du commit precedentbarras
- amelioration des messages d'erreurs de la condition de garde - reorganisation de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3457 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-17nouveau Subst:barras
- marche lorsqu'il n'y rien a reecrire - marche avec les hypotheses definies (Subst inclut l'Unfold partout) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3450 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-15Traitement spécial pour les types à l'internalisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3443 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-12Ajout du vernac Proof withgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3425 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3417 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3392 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Re-ajout constrInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3237 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14JMeq now treated as an equality by tactics.courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3232 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-06Raffinement de l'heuristique d'unification dans sig_clausale_formeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3218 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-23Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3179 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-22Correction d'une incompatibilité de nommage introduite lors du commit ↵herbelin
précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3171 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
variables introduites par NewDestruct et NewInduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3169 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
les erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3141 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-14Réparation bug Inversion (#212)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3139 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des ↵barras
letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-08Subst ne fait pas clear sur x:=efilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3103 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Oops...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3060 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Table fonctionnelle dans autorewritecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3057 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01Vraie substitutivite de autohintscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-01bug de noms long pour eqT.clrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3053 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3045 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-27passage a ocaml 3.06herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3041 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-16Subst (tout court)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3007 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-11tactique Subst x1 ... xnfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2998 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-09Code mort de AutoRewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2993 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16correction de bugs:barras
- subst_term_gen ne depliait pas les constantes locales de maniere uniforme - la tactique Simpl ne simplifiait pas les constantes definies dans le contexte de but - la conversion d'un constr vers identificateur ne prenait pas en compte les inductifs et constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2971 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13AutoRewrite substitutive...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2965 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2963 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-30Branchement de Assert, Pose et LetTac sur l'algo de création de nomsherbelin
frais de Intro git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2939 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-19correction bugs Tautocourant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2905 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17tactique Substfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2894 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-17Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2893 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-16Bug dans la globalisation des arguments de tactiques primitivesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2882 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-15Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitcourant
de la forme (E->F)->G. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2868 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-11Que la localisation des erreurs pour les tactiques atomiques marcheherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2853 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-07-03Hack pour autoriser les $n dans les Grammar tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2837 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-13Réparation de l'interprétation des fermetures (sans casser Field!)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2779 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2765 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Tentative de réparation d'un bug Omega: une variable de section qui après ↵herbelin
effacement ne peut être renommée pareille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2763 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans ↵herbelin
Simplify_eq et Injection git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2757 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-23 01:45:18 +0000