aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2003-11-08Nettoyageherbelin
2003-11-06Added Instantiate ... incorbinea
2003-11-04Amelioration message d'erreur avec pretyping; prise en compte syntactic def d...herbelin
2003-10-27Bug Double Inversionherbelin
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
2003-10-21Bug Abstract en presence de LetIn; essai d'un Assumption d'abord avec alpha-c...herbelin
2003-10-21Correction bug FreshIdherbelin
2003-10-20Globalisation des hints autorewriteherbelin
2003-10-19Extension de l'utilisation de contradictionherbelin
2003-10-18Extension de Contradiction au cas d'hypotheses ~A et A dans le contexteherbelin
2003-10-17subst marche dans les deux sensfilliatr
2003-10-16nouvelle syntaxe de ltacbarras
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 06:36:21 +0000