aboutsummaryrefslogtreecommitdiff
path: root/parsing/coqast.mli
AgeCommit message (Expand)Author
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2005-01-03HUGE COMMITsacerdot
2004-11-16Names.substitution (and related functions) and Term.subst_mps moved tosacerdot
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
2004-07-16Nouvelle en-têteherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-03Ajout delimiteurs dans les motifs de Casesherbelin
2002-10-13Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-08-10Parsingherbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
1999-12-07debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesfilliatr
1999-09-08modules Ast et Pcoqfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 04:19:45 +0000