aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extract_env.ml
AgeCommit message (Expand)Author
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-03Merge PR #10442: Reify libobject containersEmilio Jesus Gallego Arias
2019-06-28Reify libobject containersMaxime Dénès
2019-06-27[extraction] Remove not very useful call to dumpglob.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-03-27[plugins] [extraction] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-06Extraction: switch to EConstr.t as the central type to extract from.Pierre Letouzey
2018-02-27Update headers following #6543.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 21:36:04 +0000