aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
Commit message (Expand)AuthorAge
* Remove unused Failure catchGravatar Gaëtan Gilbert2017-09-29
* Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Adding a comment regarding De Bruijn universe indices in the kernel.Gravatar Pierre-Marie Pédrot2017-07-12
* Cleaning up the implementation of module 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
| * Do not add original constraints to the environment in 'with Definition' check.Gravatar Pierre-Marie Pédrot2017-07-03
|/
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\|
| * Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-26
|\|
| * Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Gravatar Pierre Letouzey2015-10-25
| * Minor module cleanup : error HigherOrderInclude was never happeningGravatar Pierre Letouzey2015-10-25
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/
* Univs: forgot a substitution in mod_typing.Gravatar Matthieu Sozeau2015-10-02
* Univs: correct handling of with in modulesGravatar Matthieu Sozeau2015-10-02
* Univs: module constraints move to universe contexts as they mightGravatar Matthieu Sozeau2015-10-02
* Modules: fix bug #4294Gravatar Matthieu Sozeau2015-07-16
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* 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
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.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
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Mod_typing : code cleanupGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Modops.destr_functor without useless envGravatar letouzey2013-07-17
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Noise for nothingGravatar pboutill2012-03-02
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03