aboutsummaryrefslogtreecommitdiff
path: root/kernel/subtyping.ml
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-14Use thunks to univ instead of lazy constr for template typingGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-19Parameterize the constant_body type by opaque subproofs.Pierre-Marie Pédrot
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-24[kernel] Compile with almost all warnings enabled.Emilio Jesus Gallego Arias
2018-07-03Subtyping.check_constant: remove unused module path argument.Gaëtan Gilbert
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
2017-07-06Merge PR #853: Clean 'with Definition' implementation.Maxime Dénès
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-07-04Removing dead code in Subtyping.Pierre-Marie Pédrot
2017-07-03Removing a few suspicious functions from the kernel.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Disable debug printingAmin Timany
2017-06-16Squashed commit of the following:Amin Timany
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-02Univs: correct handling of with in modulesMatthieu Sozeau
2015-10-02Univs: fix subtyping of polymorphic parameters.Matthieu Sozeau
2015-01-17Make native compiler handle universe polymorphic definitions.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-02Implement module subtyping for polymorphic constants (errors onMatthieu Sozeau
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.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-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:45:51 +0000