aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extraction.ml
AgeCommit message (Expand)Author
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
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-07-24Projections use index representationGaëtan Gilbert
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
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-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-23Make some functions on terms more robust w.r.t new term constructs.Maxime Dénès
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
2017-08-01Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)Maxime Dénès
2017-07-26Extraction: reduce primitive projections in types (fix bug 4709)Pierre Letouzey
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
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-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2017-01-28Remove useless commentsGaetan Gilbert
2016-12-12Extend Fast_typeops to be a replacement for TypeopsGaetan Gilbert
2016-09-29Extraction: ignore some useless stuff about universesPierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-23Fix typo.Guillaume Melquiond
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:01:45 +0000