aboutsummaryrefslogtreecommitdiff
path: root/kernel/mod_typing.ml
AgeCommit message (Expand)Author
2019-05-23Fixing typos - Part 2JPR
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2018-05-28Unify pre_env and envMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2017-12-30Returning instance instead of substitution in universe context abstraction.Pierre-Marie Pédrot
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-09-29Remove unused Failure catchGaëtan Gilbert
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-12Adding a comment regarding De Bruijn universe indices in the kernel.Pierre-Marie Pédrot
2017-07-11Cleaning up the implementation of module 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-03Do not add original constraints to the environment in 'with Definition' check.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-31Merge branch 'v8.5' into trunkGuillaume Melquiond
2015-12-22Inclusion of functors with restricted signature is now forbidden (fix #3746)Pierre Letouzey
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-28Adds support for the virtual machine to perform reduction of universe polymor...Gregory Malecha
2015-10-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-25Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Pierre Letouzey
2015-10-25Minor module cleanup : error HigherOrderInclude was never happeningPierre Letouzey
2015-10-06Splitting kernel universe code in two modules.Pierre-Marie Pédrot
2015-10-02Univs: forgot a substitution in mod_typing.Matthieu Sozeau
2015-10-02Univs: correct handling of with in modulesMatthieu Sozeau
2015-10-02Univs: module constraints move to universe contexts as they mightMatthieu Sozeau
2015-07-16Modules: fix bug #4294Matthieu Sozeau
2015-03-25Fix vm compiler to refuse to compile code making use of inductives withMatthieu Sozeau
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
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-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Mod_typing : code cleanupletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-08State Transaction Machinegareuselesinge
2013-07-17Modops.destr_functor without useless envletouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of Labelppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:43:41 +0000