aboutsummaryrefslogtreecommitdiff
path: root/interp/dumpglob.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29Avoid Dumpglob dependency on Lexerletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-10-29Fixed broken globalization of identifiers containing utf8 lettersherbelin
2011-10-29Added checksums to glob files and warned about possibly missingherbelin
2010-12-04Fixing several bugs with links to notation in coqdoc, including bug #2445:herbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-08Some dead code removal + cleanupsletouzey
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