aboutsummaryrefslogtreecommitdiff
path: root/checker/subtyping.ml
AgeCommit message (Expand)Author
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-10-09[coqchk] Fix checking of records in module signaturesVincent Laporte
2018-07-24Projections use index representationGaëtan Gilbert
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-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
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 checker.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin 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-05-31Checker: avoid using obsolete names from NamesPierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2014-12-17Update checker/values and cic due to changes in case_info and record_body.Matthieu Sozeau
2014-09-05Rename eta_expand_ind_stacks, fix the one from the checker and adaptMatthieu Sozeau
2014-06-07Removing 'open Univ' from checker.Pierre-Marie Pédrot
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2013-10-24Get rid of polymorphic equality in "checker/subtyping.ml".xclerc
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-19Dir_path --> DirPathletouzey
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-10-06still some more dead code removalletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-08-08Updating headers.herbelin
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-02Noise for nothingpboutill
2011-10-26Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)letouzey
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-04-12Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2010-09-24Checker: remove some dead codeletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:51:18 +0000