aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_tactic.ml4
AgeCommit message (Expand)Author
2000-12-06Extension de la syntaxe de LetTacherbelin
2000-12-06Correction pour les qualidconstargdelahaye
2000-12-05Plus de quote devant les ident et les ?delahaye
2000-11-28Elimination du 'delahaye
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel in...herbelin
2000-11-23Bug qualidconstarg (intervient pour Transparent)herbelin
2000-11-20Nouvelle entrée qualidarg pour noms qualifiés; nouveau lexeme METAIDENT pou...herbelin
2000-11-03compilation des fichiers ml4 sans GNUseriesfilliatr
2000-10-30Priorite du Try/Orelse + Debug switch + correction bug dans Patterndelahaye
2000-10-03Ajout castedopenconstrarg; Renommage tactique Let en LetTacherbelin
2000-08-17Pattern matching de sous-termes + exceptions dans le lexerdelahaye
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
2000-05-03Ajout du langage de tactiquesdelahaye
2000-01-26Fin du changement comarg -> constrargherbelin
2000-01-13Nettoyage des fichiers de parsingherbelin
2000-01-07Renommage command en constrherbelin
1999-12-13 - états fabriqués avec -silentfilliatr
1999-12-02modifs pour premiere edition de liensfilliatr
1999-09-08compilation des grammaires (ouf)filliatr
1999-09-08modules grammaire Coqfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 22:44:48 +0000