aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernac.mli
AgeCommit message (Expand)Author
2010-02-12Delineating a API for Coq inside toplevel/vernac.mlvgross
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2004-07-16Nouvelle en-têteherbelin
2004-03-26Ajout entree pour exporter les debuts et fins de compilation en mode -xmlherbelin
2004-02-12Localisation des erreurs d'internalisation des notations de tactiquesherbelin
2003-02-11Undo dans Coq IDEfilliatr
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-09-18Ajout d'une option et d'une fonction compile pour fabriquer les .voherbelin
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
1999-09-28corrections pour ocamlwebfilliatr
1999-09-28retablissement du toplevelfilliatr