aboutsummaryrefslogtreecommitdiff
path: root/kernel/mod_typing.ml
AgeCommit message (Expand)Author
2020-10-11Pick the universe graph out of the environment in conversion API.Pierre-Marie Pédrot
2020-08-18Rename VM-related kernel/cfoo files to kernel/vmfooGaëtan Gilbert
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:39:56 +0000