coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunately	Hugo Herbelin	2014-04-29
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	Fix guard condition for nested cofixpoints in checker.	Maxime Dénès	2014-04-10
*	printer for coqchk	Enrico Tassi	2014-04-08
*	Fixing coqchk. It was my fault, I misused canonical and user equalities	Pierre-Marie Pédrot	2014-04-04
*	Printing backtraces in coqchk while in debug mode.	Pierre-Marie Pédrot	2014-03-18
*	Fixing checker with respect to new kernel name structure and hashmaps.	Pierre-Marie Pédrot	2014-03-18
*	vi2vo: universes handling finally fixed	Enrico Tassi	2014-03-11
*	Adding a canary library. This canary is imperfect. It allows serialization	Pierre-Marie Pédrot	2014-03-05
*	Added a new module HMap. It works (almost) like Map, except that it expects	Pierre-Marie Pédrot	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot	2014-03-05
*	checker and votour ported to new vo format (after -vi2vo)	Enrico Tassi	2014-02-26
*	votour: better error messages	Enrico Tassi	2014-02-26
*	checker: less useless error messages	Enrico Tassi	2014-02-26
*	fix checker w.r.t. mutual_inductive_body and constant_body	Enrico Tassi	2014-02-26
*	fix checker w.r.t. Dyn.t validation	Enrico Tassi	2014-02-26
*	Fixing checker compilation, which was broken by the following commit:	Pierre-Marie Pédrot	2014-01-19
*	Relaxing the sort elimination check to allow for let-bindings in arities.	Maxime Dénès	2014-01-18
*	Christmas is over...	Maxime Dénès	2014-01-15
*	.vi files: .vo files without proofs	Enrico Tassi	2014-01-04
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	inductive.ml : get rid of some obvious (Lazy.force (lazy t))	letouzey	2013-10-24
*	Rtree : cleanup of the comparing code	letouzey	2013-10-24
*	Get rid of polymorphic equality in "checker/subtyping.ml".	xclerc	2013-10-24
*	Turn many List.assoc into List.assoc_f	letouzey	2013-10-24
*	cList.index is now cList.index_f, same for index0	letouzey	2013-10-23
*	Future: ported to Ephemeron + exception enhancing	gareuselesinge	2013-10-18
*	Ephemeron: marshaling friendly keys	gareuselesinge	2013-10-18
*	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
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Adding dynamic value printing to votour through a registering mechanism.	ppedrot	2013-08-23
*	Misc changes around coqtop.ml :	letouzey	2013-08-22
*	Change in vo format : digest aren't Marshalled anymore	letouzey	2013-08-22
*	Fixing votour	ppedrot	2013-08-20
*	Fix compilation of coqcheck	gareuselesinge	2013-08-20
*	Declarations.mli: reorganization of modular structures	letouzey	2013-08-20
*	Repair coqcheck : constant_body constraints are also future	letouzey	2013-08-20
*	checker validation fixed w.r.t. Futures	gareuselesinge	2013-08-09
*	checker validation made a bit more verbose	gareuselesinge	2013-08-09
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Declaremods: major refactoring, stop duplicating libobjects in modules	letouzey	2013-07-17
*	Added a generic notion of hook. Hooks are functions to be set	ppedrot	2013-05-12
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	Remove deprecated option -no-hash-consing (currently doing nothing)	letouzey	2013-04-23
*	Checker: vo validation checks the absence of Var/Evar/Meta	letouzey	2013-04-15
*	Checker : a md5-based way to ensure checker/values.ml is always in sync	letouzey	2013-04-15