aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/dumpglob.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* [safe_string] interp/dumpglobGravatar Emilio Jesus Gallego Arias2017-03-14
* coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\
| * Fix incorrect glob data for module symbols (bug #2336).Gravatar Guillaume Melquiond2016-08-18
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/
* Increase the size of the dumpglob buffer for cooking notations (bug #4708).Gravatar Guillaume Melquiond2016-05-04
* Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Do not dump a glob reference when its location is ghost. (Fix bug #4469)Gravatar Guillaume Melquiond2015-12-31
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing what really looks like a bug in the initial implementation ofGravatar Hugo Herbelin2014-10-22
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Have the feedback bus as a backend for dumping globs.Gravatar Carst Tankink2014-04-10
* Dumpglob: factor out reference dumping.Gravatar Carst Tankink2014-04-10
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* minor cleanup in coqtop.mlGravatar letouzey2013-04-23
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Fixed broken globalization of identifiers containing utf8 lettersGravatar herbelin2011-10-29
* Added checksums to glob files and warned about possibly missingGravatar herbelin2011-10-29
* Fixing several bugs with links to notation in coqdoc, including bug #2445:Gravatar herbelin2010-12-04
* 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