aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2002-06-05Rpercussion de la possibilit de mettre des hyps quantifies dans Simplify_eq e...herbelin
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
2002-05-31Les VContext ne sont plus des fermetures (temporaire)delahaye
2002-05-30Nettoyageherbelin
2002-05-30Finalement un seul constr pour l'instant dans ExtraRedExprherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Réorganisation des tclTHEN (cf dev/changements.txt)herbelin
2002-05-29Fichiers tactics/*.ml4 remplacent les tactics/*.vherbelin
2002-05-29Pour les tactiques dépendant de Falseherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 04:07:10 +0000