aboutsummaryrefslogtreecommitdiff
path: root/parsing/pptactic.ml
AgeCommit message (Expand)Author
2004-07-16Nouvelle en-têteherbelin
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-28more evar stuffcorbinea
2004-05-27Bug affichage ClearBodyherbelin
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...herbelin
2004-03-17Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...herbelin
2004-03-02Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...herbelin
2004-03-02Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...herbelin
2004-03-01Généralisation du type ltac Identifier en IntroPattern; prise en compte des...herbelin
2004-01-09bugs avec Pose et Assertbarras
2003-12-24Bug affichage Decomposeherbelin
2003-12-17ajout test de non-regression Clear d'une def localebarras
2003-12-01Nouvelle tactique EExistsclrenard
2003-11-25Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...herbelin
2003-11-17New tactics : econstructor, eleft, eright, esplitclrenard
2003-11-13factorisation et generalisation des clausesbarras
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la biblio...herbelin
2003-11-12Idtac peut prendre un argument à affichernarboux
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-06Added Instantiate ... incorbinea
2003-11-02Le printeur de Show Script n'etait pas le bon en v7herbelin
2003-11-01Traduction des noms pour les refs de pr_glob_generic (via pr_global)herbelin
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par...herbelin
2003-10-17Traduction des idents aussi dans le printer generique des tactiquesherbelin
2003-10-16nouvelle syntaxe de ltacbarras
2003-10-10Cablage en dur de inversionherbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-09-18Simplification afficheur de tactiques non primitiveherbelin
2003-09-16En attendant l'afficheur...herbelin
2003-09-09Traduction des réferences arguments de commandes non primitivesherbelin
2003-09-06Bug affichage tactiques supplementaires en v8 (suite)herbelin
2003-09-05Bug affichage tactiques supplementaires en v8herbelin
2003-06-19Ajout 'Symmetry in Hyp'herbelin
2003-06-13Utilisation de intro_pattern dans NewDestruct/NewInductionherbelin
2003-05-24Ajout FreshIdherbelin
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-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-27Reparation affichage LetTacherbelin
2003-04-14Localisation des appels de tactiques définies sans argumentsherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-04-02espace manquantherbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-12*** empty log message ***barras
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-09Ajout Simpl et Change sur des sous-termesherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 14:34:09 +0000