aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/mod_checking.ml
Commit message (Expand)AuthorAge
* 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
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* make validate repaired via a temporary fix for #2949Gravatar letouzey2013-02-13
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* still some more dead code removalGravatar letouzey2012-10-06
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* Noise for nothingGravatar pboutill2012-03-02
* Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)Gravatar letouzey2011-10-26
* ported r14149 from v8.3 branch: bug in checker (redefined global)Gravatar barras2011-05-23
* 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
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Checker: remove some dead codeGravatar letouzey2010-09-24
* Sharing is not anymore broken by traverse_module.Gravatar soubiran2010-09-15
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* porting r11900 11905 and 11953 to trunkGravatar barras2009-03-02
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...Gravatar barras2008-09-02
* fixed bug with aliasesGravatar barras2008-05-07
* checker deals with polymorphic constants and module aliasesGravatar barras2008-05-06
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21