aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.mli
Commit message (Expand)AuthorAge
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Cleanning and factorizing code in funind. Spliting new_arg_principles into to...Gravatar jforest2006-05-03
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Nouvelle en-têteGravatar herbelin2004-07-16
* Deplacement pr_subgoal and co vers PfeditGravatar herbelin2003-10-13
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* 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
* Suite de la suppression : enamed_declaration est remplace par evar_map.Gravatar clrenard2001-11-06
* Suppression option immediate_discharge; nettoyage de Declare et conséquencesGravatar herbelin2001-10-11
* entetesGravatar filliatr2001-03-15
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
* export a function that is needed in pcoq.Gravatar bertot2001-02-13
* exported several functions that are used in the graphical interface pcoq.Gravatar bertot2001-02-09
* export a function that can be used to retrieve the context correspondingGravatar bertot2001-02-08
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
* Uniformisation AddPath, Print LoadPath, ... en Add Path, Print Path. Abstract...Gravatar herbelin2000-09-10
* documentation interfacesGravatar filliatr1999-12-13
* module MetasyntaxGravatar filliatr1999-12-01
* Vernacinterp et Vernacentries (partiellement)Gravatar filliatr1999-11-24