coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix the checker by merely adapting the data structure.	Pierre-Marie Pédrot	2018-06-07
*	Moving Rtree.smart_map into Rtree.Smart.map.	Hugo Herbelin	2018-05-23
*	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
*	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
*	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
*	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
*	[checker] Avoid relying on canonical names.	Maxime Dénès	2018-01-25
*	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29
*	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Remove some unused values and types	Gaetan Gilbert	2017-04-27
*	Locally disable some warnings.	Gaetan Gilbert	2017-04-27
*	Checker: avoid using obsolete names from Names	Pierre Letouzey	2016-05-31
*	CLEANUP: Simplifying the changes done in "checker/*"	Matej Kosik	2016-02-15
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Checker was forgetting to register global universes introduced by opaque	Matthieu Sozeau	2015-11-04
*	Checker: Fix bug #4282	Matthieu Sozeau	2015-07-07
*	Fix checker after addition of a universe context in with t := c constraints.	Matthieu Sozeau	2015-02-26
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Removing dead code in checker/univ.ml.	Pierre-Marie Pédrot	2014-06-10
*	Adapt the checker to polymorphic universes and projections (untested).	Matthieu Sozeau	2014-05-08
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
*	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc	2013-10-14
*	Slightly more compact representation of 'a substituted type,	ppedrot	2013-09-14
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Checker: empty sections hardcoded in cb and mind	letouzey	2013-04-15
*	Checker: reified encoding of .vo types in values.ml	letouzey	2013-04-15
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	Mod_subst.force: avoid using join when only one subst	letouzey	2013-04-02
*	Minor cleanup concerning Mod_subst.MBImap	letouzey	2013-04-02
*	Restrict (try...with...) to avoid catching critical exn (part 2)	letouzey	2013-03-12
*	More monomorphization.	ppedrot	2013-03-05
*	Names: Modularize constant and mutual_inductive	letouzey	2013-02-26
*	Checker: re-sync vo structures after Maxime's commit 16136	letouzey	2013-02-12
*	Modulification of mod_bound_id	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	still some more dead code removal	letouzey	2012-10-06
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	Noise for nothing	pboutill	2012-03-02
*	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey	2011-04-03
*	Propagate recent kernel changes to the checker	letouzey	2011-03-03
*	A fine-grain control of inlining at functor application via priority levels	letouzey	2011-01-31
*	Checker: remove some dead code	letouzey	2010-09-24