aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extract_env.ml
AgeCommit message (Expand)Author
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-10-04Extraction : minor support stuff for the new Extraction Compute pluginPierre Letouzey
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-26Merge PR #857: Extraction: various fixes related with bug 4720Maxime Dénès
2017-07-26Merge PR #859: Extraction TestCompileMaxime Dénès
2017-07-20Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)Pierre Letouzey
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-05Extraction TestCompile foo : a new command for extraction + ocamlcPierre Letouzey
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-10Remove (useless) aliases from the API.Matej Košík
2017-06-07Put all plugins behind an "API".Matej Kosik
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-03-21[extraction] Flush formatters at end of output.Emilio Jesus Gallego Arias
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-02-07Extraction: remove the "print to devnull" hack now that pp isn't lazy anymorePierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-04Extraction: msg_notice instead of msg_info.Pierre Courtieu
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-12-14Extraction: cosmetically avoid generating spaces on empty linesPierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-12-12Extraction: fix for bug #4334 (use of delta_resolver in Extract_env)Pierre Letouzey
2015-04-09Add extraction to JSON.Nickolai Zeldovich
2015-03-21Properly capitalize filenames when extracting to Haskell. (Fix for bug #3221)Guillaume Melquiond
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: discard code unnecessary to fulfill a module signaturePierre Letouzey
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-11Extraction: discard unnecessary code inside modules without signaturesPierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-07-17Lib.contents () instead of Lib.contents_after Noneletouzey
2013-07-17Extraction : message about lack of support for toplevel Includeletouzey
2013-03-15Extract_env : correct exceptions mentionned in a try ... withletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 9)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)letouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:46:04 +0000