aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.mli
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2008-02-22Merge with lmamane's private branch:lmamane
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into to...jforest
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-16Nouvelle en-têteherbelin
2003-10-13Deplacement pr_subgoal and co vers Pfeditherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2001-11-06Suite de la suppression : enamed_declaration est remplace par evar_map.clrenard
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-13export a function that is needed in pcoq.bertot
2001-02-09exported several functions that are used in the graphical interface pcoq.bertot
2001-02-08export a function that can be used to retrieve the context correspondingbertot
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-09-10Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...herbelin
1999-12-13documentation interfacesfilliatr
1999-12-01module Metasyntaxfilliatr
1999-11-24Vernacinterp et Vernacentries (partiellement)filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 00:43:11 +0000