aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/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
* 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 checker.Gravatar Pierre-Marie Pédrot2017-07-11
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Correct coqchk reductionGravatar 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
* Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
* Rename eta_expand_ind_stacks, fix the one from the checker and adaptGravatar Matthieu Sozeau2014-09-05
* Removing 'open Univ' from checker.Gravatar Pierre-Marie Pédrot2014-06-07
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
* Get rid of polymorphic equality in "checker/subtyping.ml".Gravatar xclerc2013-10-24
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Checker: empty sections hardcoded in cb and mindGravatar letouzey2013-04-15
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* still some more dead code removalGravatar letouzey2012-10-06
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-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
* Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)Gravatar letouzey2011-10-26
* 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
* Checker: remove some dead codeGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 07:46:16 +0000