aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/declarations.ml
Commit message (Expand)AuthorAge
* Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
* [checker] Avoid relying on canonical names.Gravatar Maxime Dénès2018-01-25
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
* Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* CLEANUP: Simplifying the changes done in "checker/*"Gravatar Matej Kosik2016-02-15
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
* Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
* Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a field ci_cstr_nargs to case_info and mind_consnrealargs toGravatar Hugo Herbelin2014-04-28
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Checker: empty sections hardcoded in cb and mindGravatar letouzey2013-04-15
* 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
* Mod_subst.force: avoid using join when only one substGravatar letouzey2013-04-02
* Minor cleanup concerning Mod_subst.MBImapGravatar letouzey2013-04-02
* Restrict (try...with...) to avoid catching critical exn (part 2)Gravatar letouzey2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* 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
* still some more dead code removalGravatar letouzey2012-10-06
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Noise for nothingGravatar pboutill2012-03-02
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Propagate recent kernel changes to the checkerGravatar letouzey2011-03-03
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Checker: remove some dead codeGravatar letouzey2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fix likely semantic typosGravatar glondu2010-09-15
* 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