aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
AgeCommit message (Expand)Author
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
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
2018-12-12Higher-level libobject API for objects with fixed scopesMaxime Dénès
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28Add extraction directives for nicer extraction of bytesJason Gross
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-02[ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0Emilio Jesus Gallego Arias
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-07-25Merge PR #8063: Direct implementation of Ascii.eqb and String.eqb (take 2)Hugo Herbelin
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-16Add Extract Inlined Constant directives for {String,Ascii}.eqbJason Gross
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:02:21 +0000