aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2003-10-13Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...herbelin
2003-10-13Deplacement next_global_ident_away dans Termopsherbelin
2003-10-11Uniformisation comportement decompEq pour corriger un bug introduit dans le I...herbelin
2003-10-11Bug calcul du nom de la premiere equationherbelin
2003-10-11Death of 'a somewhat cryptic module'herbelin
2003-10-11Death of 'a somewhat cryptic module'herbelin
2003-10-10Typoherbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
2003-10-10Dead of 'a somewhat cryptic module'herbelin
2003-10-10Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...herbelin
2003-10-10Unification lemInv et lemInv_inherbelin
2003-10-10Cablage en dur de inversionherbelin
2003-10-10Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'herbelin
2003-10-10Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-08Bug utilisation nametab pour ltacherbelin
2003-10-08Des abbreviations pour constrintern.ml; generic argument IdentArgherbelin
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
2003-09-23Correction bug NewInduction pour les inductifs de type 'ordinaux'herbelin
2003-09-23Bug internalisation des Extern: la globalisation doit etre stricteherbelin
2003-09-22Passage à la V8 par défautherbelin
2003-09-18Interface Eautoherbelin
2003-09-12Indépendance vis à vis de Declareherbelin
2003-09-11Nettoyageherbelin
2003-09-09Protection traducteur contre meta de Grammar tacticherbelin
2003-08-11Nouvelle mouture du traducteur v7->v8herbelin
2003-07-03switching back to old tautocorbinea
2003-07-02added hints into Groundcorbinea
2003-07-02suppression de newtautocorbinea
2003-06-27*** empty log message ***courant
2003-06-25Une completion de l'interpretation des TacAlias pour la partie interpretableherbelin
2003-06-20Ground Update.corbinea
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-14Ajout option Local à Hint, Hints et HintDestructherbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-06-12Ajout option translate_syntax pour caractériser l'interprétation du traduct...herbelin
2003-06-10Traducteur + passage des noms de tactiques à kernel_name pour compatibilité...herbelin
2003-05-25Ground and CCsolve updatescorbinea
2003-05-24Amélioration affichage locations; prise en compte variables dans lettac; ajo...herbelin
2003-05-22Réparation d'un bug de backtracking qui lui-même succédait à une ineffica...herbelin
2003-05-22Preservation affichage des ?n en V7herbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...herbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-05-19Restructuration des procédures de filtrageherbelin
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
2003-05-07Enhancement of the Ground tactic, addition of GTauto and GIntuition.corbinea
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-25Added the Ground tactic.corbinea
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 19:45:52 +0000