aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extract_env.ml
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Gravatar Maxime Dénès2018-03-08
|\
| * An experimental 'Show Extraction' command (grant feature wish #4129)Gravatar Pierre Letouzey2018-03-06
| * Extraction: switch to EConstr.t as the central type to extract from.Gravatar Pierre Letouzey2018-03-06
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Extraction : minor support stuff for the new Extraction Compute pluginGravatar Pierre Letouzey2017-10-04
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Merge PR #857: Extraction: various fixes related with bug 4720Gravatar Maxime Dénès2017-07-26
|\
* \ Merge PR #859: Extraction TestCompileGravatar Maxime Dénès2017-07-26
|\ \
| | * Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Gravatar Pierre Letouzey2017-07-20
| |/ |/|
* | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
| * Extraction TestCompile foo : a new command for extraction + ocamlcGravatar Pierre Letouzey2017-07-05
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* [extraction] Flush formatters at end of output.Gravatar Emilio Jesus Gallego Arias2017-03-21
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
* Extraction: remove the "print to devnull" hack now that pp isn't lazy anymoreGravatar Pierre Letouzey2017-02-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 17:48:27 +0000