aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/environ.mli
Commit message (Expand)AuthorAge
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Checker: get rid of code handling section variablesGravatar letouzey2013-04-15
* Checker: empty sections hardcoded in cb and mindGravatar letouzey2013-04-15
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)Gravatar letouzey2011-10-26
* Checker: remove some dead codeGravatar letouzey2010-09-24
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* porting r11900 11905 and 11953 to trunkGravatar barras2009-03-02
* fixed dependency problems with the checkerGravatar barras2008-05-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 19:08:10 +0000