aboutsummaryrefslogtreecommitdiff
path: root/interp/dumpglob.mli
AgeCommit message (Expand)Author
2016-09-22coqc -o now places .glob file near .vo fileEnrico Tassi
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-07-11Export type_of_global_ref (useful for external users of glob files)Enrico Tassi
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2013-08-22Misc changes around coqtop.ml :letouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-08-08Updating headers.herbelin
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-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-02Noise for nothingpboutill
2011-10-29Added checksums to glob files and warned about possibly missingherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Constrintern: unified push_name_env and push_loc_name_env; madeherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2008-07-24Suite commit 11236notin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 06:17:01 +0000