aboutsummaryrefslogtreecommitdiff
path: root/interp/dumpglob.mli
AgeCommit message (Expand)Author
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-07-03Move variable_secpath logic to dumpglob from constrinternGaëtan Gilbert
2019-07-01[dumpglob] Move dumpglob-specific data to dumpglob.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
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-01-31 09:40:21 +0000