aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/subtyping.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Properly handling polymorphic inductive subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* Merge PR #853: Clean 'with Definition' implementation.Gravatar Maxime Dénès2017-07-06
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Removing dead code in Subtyping.Gravatar Pierre-Marie Pédrot2017-07-04
| * Removing a few suspicious functions from the kernel.Gravatar Pierre-Marie Pédrot2017-07-03
|/
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Disable debug printingGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Univs: correct handling of with in modulesGravatar Matthieu Sozeau2015-10-02
* Univs: fix subtyping of polymorphic parameters.Gravatar Matthieu Sozeau2015-10-02
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Implement module subtyping for polymorphic constants (errors onGravatar Matthieu Sozeau2014-10-02
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* Fixing bug #2466Gravatar ppedrot2013-02-24
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14