aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/coqast.ml
Commit message (Expand)AuthorAge
* HUGE COMMITGravatar sacerdot2005-01-03
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Ajout delimiteurs dans les motifs de CasesGravatar herbelin2002-11-03
* Première proposition d'un type ML exprimant la syntaxe de constr; nettoyageGravatar herbelin2002-10-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29
* ParsingGravatar herbelin2001-08-10
* entetesGravatar filliatr2001-03-15
* debuggage inductifs (suite) / compilation Dhyp et Auto (mais pas linkesGravatar filliatr1999-12-07
* modules Ast et PcoqGravatar filliatr1999-09-08