aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction/extraction.ml
AgeCommit message (Expand)Author
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
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-30Extraction : add a location in the error message about polypropPierre Letouzey
2016-05-23Extraction/Projections: Fix bug #4710Matthieu Sozeau
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Handle primitive projections inside types when extracting (bug #4616).Guillaume Melquiond
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-12-15Extraction: more cautious use of intermediate result caching (fix #3923)Pierre Letouzey
2015-12-12Extraction: nicer implementation of ImplicitsPierre Letouzey
2015-12-07Fix some typos.Guillaume Melquiond
2015-07-22Extraction: fix primitive projection extraction.Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Extraction: no more ascii blob in type variables (fix #3227)Pierre Letouzey
2015-01-11Extraction : some more support functions for a future "Extraction Compute"Pierre Letouzey
2015-01-11Extraction: minor tweaks to ease ongoing experiments about LambdaPierre Letouzey
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-01A tentative uniform naming policy in module Inductiveops.Hugo Herbelin
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Fix a pervasive equality use.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-03Fixing Pervasives.equality in extraction.Pierre-Marie Pédrot
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:26:59 +0000