aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-11-22Bug introduit avec le 'Simpl f'herbelin
2003-11-18Blindage vis a vis des constructeurs partiellement appliquesherbelin
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-11-15Bug nommage destructherbelin
2003-11-14Move des hyps de NewInduction: retour a situation V7.4 a defaut d'etre robusteherbelin
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12Prise en compte des alias syntaxiques vers des references dans divers lieux d...herbelin
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-12petits changements de syntaxebarras
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local def; simplif...herbelin
2003-11-09'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...herbelin
2003-11-08Code obsoleteherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:41:36 +0000