aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2002-12-24code mortherbelin
2002-12-23Re-essai de forcer le terme réécrit à apparaître dans le butherbelin
2002-12-21Backtrack sur la tentative d'interdire les K-abstractions dans l'unificationherbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-19suite du commit precedentbarras
2002-12-17nouveau Subst:barras
2002-12-15Traitement spécial pour les types à l'internalisationherbelin
2002-12-12Ajout du vernac Proof withgregoire
2002-12-10Normalisation beta-iota du type du terme appliqué (fait avant dans Typing)herbelin
2002-12-09Option pour rendre les vérifications du refiner optionnelleherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-11-14Re-ajout constrInherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-14JMeq now treated as an equality by tactics.courant
2002-11-06Raffinement de l'heuristique d'unification dans sig_clausale_formeherbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-10-23Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Localherbelin
2002-10-22Correction d'une incompatibilité de nommage introduite lors du commit précÃ...herbelin
2002-10-21Ajout d'un suffixe "as [ names ]" pour nommer manuellement lesherbelin
2002-10-21NewDestruct/NewInduction acceptent l'option "using"herbelin
2002-10-14L'application de ltac attend une référence; meilleure protection contreherbelin
2002-10-14Réparation bug Inversion (#212)herbelin
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des le...barras
2002-10-08Subst ne fait pas clear sur x:=efilliatr
2002-10-01Oops...coq
2002-10-01Table fonctionnelle dans autorewritecoq
2002-10-01Vraie substitutivite de autohintscoq
2002-10-01bug de noms long pour eqT.clrenard
2002-09-29Que des niveaux d'univers frais dans le type des constantes globalesherbelin
2002-09-27passage a ocaml 3.06herbelin
2002-09-16Subst (tout court)filliatr
2002-09-11tactique Subst x1 ... xnfilliatr
2002-09-09Code mort de AutoRewriteherbelin
2002-08-16correction de bugs:barras
2002-08-13AutoRewrite substitutive...coq
2002-08-13Renoncement à distinguer les types "constr" et "types"; nettoyageherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-30Branchement de Assert, Pose et LetTac sur l'algo de création de nomsherbelin
2002-07-19correction bugs Tautocourant
2002-07-17tactique Substfilliatr
2002-07-17Nettoyage de code pour la règle [id:(?1-> ?2)-> ?3|- ?]corbinea
2002-07-16Bug dans la globalisation des arguments de tactiques primitivesherbelin
2002-07-15Correction bug Tauto : la regle pour (A->B)->C echouait quand C etaitcourant
2002-07-11Que la localisation des erreurs pour les tactiques atomiques marcheherbelin
2002-07-03Hack pour autoriser les $n dans les Grammar tacticherbelin
2002-06-13Réparation de l'interprétation des fermetures (sans casser Field!)herbelin
2002-06-06Ajout coercion constr vers hyp quantifiéeherbelin
2002-06-06Tentative de réparation d'un bug Omega: une variable de section qui après e...herbelin
2002-06-06Passage de PatternMatchingFailure vers UserError pour capture par tclFIRSTherbelin
2002-06-05Repercussion de la possibilit de mettre des hyps quantifiees dans Simplify_eq...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 10:55:19 +0000