aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-11-23Fix comparison of extracted array literalsGaëtan Gilbert
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-21Deprecate the non-qualified equality functions on kerpairs.Pierre-Marie Pédrot
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-18Extraction: At declaration point of a global, use its declaring name.Hugo Herbelin
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-26[declare] Reify Proof.t API into the Proof module.Emilio Jesus Gallego Arias
2020-06-26[declare] Move proof information to declare.Emilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
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-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:00:42 +0000