aboutsummaryrefslogtreecommitdiff
path: root/interp/dumpglob.ml
AgeCommit message (Expand)Author
2008-10-14Dumpglob.dump_modref : fix an assert failureletouzey
2008-07-24Suite commit 11236notin
2008-07-23Stop glob messages to be printed by default on stdout letouzey
2008-07-22Oubli lors du commit #11236notin
2008-07-21Suite commit 11236notin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-07-07Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...notin
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin