aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
2020-02-18Merge PR #11529: [build] Consolidate stdlib's .v files under a single directory.Théo Zimmermann
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-01-30Do not rely on Libobject for the current environment in extraction.Pierre-Marie Pédrot
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
2020-01-08Factorize ascii extraction in ExtrOcamlChar.vMaxime Dénès
2020-01-08Better extraction of string literals in HaskellMaxime Dénès
2020-01-08Reimplement string <-> char list conversionsXavier Leroy
2020-01-08Typo in commentXavier Leroy
2020-01-08Rename ExtrOcamlStringPlus into ExtrOcamlNativeStringXavier Leroy
2020-01-08Avoid hardcoded paths in extractionMaxime Dénès
2020-01-08Avoid warning 40Maxime Dénès
2020-01-08Support extraction of Coq's string type to OCaml's string type, continuedXavier Leroy
2020-01-08Support extraction of Coq's string type to OCaml's string typeXavier Leroy
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-11-01Add some doc snippet in ExtrOCamlFloats.vErik Martin-Dorel
2019-11-01Add extraction for primitive floatsErik Martin-Dorel
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-23Merge PR #10897: Fix coq#4741: Extract Constant/Inductive with JSONVincent Laporte
2019-10-14Fix coq#4741: Extract Constant/Inductive with JSONHelge Bahmann
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-07-31Fix #7348: extraction of dependent record projectionsKazuhiko Sakaguchi
2019-07-22[Int63] Implement all primitives in OCamlVincent Laporte
2019-07-22[Extraction] Add support for primitive integersVincent Laporte
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-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-17Merge PR #10362: Kernel-side delaying of polymorphic opaque constantsGaëtan Gilbert
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-17Allow to delay polymorphic opaque constants.Pierre-Marie Pédrot
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 2JPR
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-03-27[plugins] [extraction] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:29:54 +0000