aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/dumpglob.ml
Commit message (Expand)AuthorAge
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Dumpglob.dump_modref : fix an assert failureGravatar letouzey2008-10-14
* Suite commit 11236Gravatar notin2008-07-24
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* Oubli lors du commit #11236Gravatar notin2008-07-22
* Suite commit 11236Gravatar notin2008-07-21
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 17:51:33 +0000