aboutsummaryrefslogtreecommitdiff
path: root/interp/dumpglob.ml
AgeCommit message (Expand)Author
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
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-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio 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-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-02-04Primitive integersMaxime Dénès
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-05-23[api] Move `Vernacexpr` to parsing.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-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-03-14[safe_string] interp/dumpglobEmilio Jesus Gallego Arias
2016-09-22coqc -o now places .glob file near .vo fileEnrico Tassi
2016-08-21Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-08-18Fix incorrect glob data for module symbols (bug #2336).Guillaume Melquiond
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-04Increase the size of the dumpglob buffer for cooking notations (bug #4708).Guillaume Melquiond
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-20Update copyright headers.Maxime Dénès
2015-12-31Do not dump a glob reference when its location is ghost. (Fix bug #4469)Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2014-10-22Fixing what really looks like a bug in the initial implementation ofHugo Herbelin
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-10Have the feedback bus as a backend for dumping globs.Carst Tankink
2014-04-10Dumpglob: factor out reference dumping.Carst Tankink
2013-08-22Misc changes around coqtop.ml :letouzey
2013-04-23minor cleanup in coqtop.mlletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:59:03 +0000