aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/declarations.mli
Commit message (Expand)AuthorAge
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Checker: reified encoding of .vo types in values.mlGravatar 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
* Checker: re-sync vo structures after Maxime's commit 16136Gravatar letouzey2013-02-12
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Checker: remove some dead codeGravatar letouzey2010-09-24
* adpated the checker to handle coomutative cuts and lazynessGravatar barras2010-07-30
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* added validation of delta_resolver (which seem to have an impact on typing)Gravatar barras2010-02-19
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Transfers to checker ("let"s in inductive arities + Coq root read-only).Gravatar herbelin2009-08-22
* 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 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