aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extract_env.ml
Commit message (Expand)AuthorAge
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Extraction: msg_notice instead of msg_info.Gravatar Pierre Courtieu2016-01-04
* Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* Extraction: cosmetically avoid generating spaces on empty linesGravatar Pierre Letouzey2015-12-14
* Extraction: nicer implementation of ImplicitsGravatar Pierre Letouzey2015-12-12
* Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Gravatar Pierre Letouzey2015-12-12
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
* Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Gravatar Guillaume Melquiond2015-03-21
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Extraction: discard code unnecessary to fulfill a module signatureGravatar Pierre Letouzey2015-01-11
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Extraction: discard unnecessary code inside modules without signaturesGravatar Pierre Letouzey2015-01-11
* Extraction : some more support functions for a future "Extraction Compute"Gravatar Pierre Letouzey2015-01-11
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* Extraction : message about lack of support for toplevel IncludeGravatar letouzey2013-07-17
* Extract_env : correct exceptions mentionned in a try ... withGravatar letouzey2013-03-15
* Restrict (try...with...) to avoid catching critical exn (part 9)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Extraction: avoid initial strange empty comments after Arnaud's hackGravatar letouzey2012-10-30
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Experimental support for a comment in the files' preamble in extraction.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Vecnacentries.dump_global silently ignores exceptionsGravatar pboutill2012-08-06
* Dump references in ExtractionGravatar pboutill2012-08-05
* More cleaningGravatar ppedrot2012-06-01
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26