coq - The formal proof system

Age	Commit message (Expand)	Author
2014-06-17	Removing dead code.	Pierre-Marie Pédrot
2014-06-04	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau
2014-05-09	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau
2014-05-08	Avoid allocations in type_of_inductive	Matthieu Sozeau
2014-05-06	- Rename eq to equal in Univ, document new modules, set interfaces.	Matthieu Sozeau
2014-05-06	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau
2014-05-06	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-28	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin
2014-04-10	Fix guard condition for nested cofixpoints.	Maxime Dénès
2014-01-18	Relaxing the sort elimination check to allow for let-bindings in arities.	Maxime Dénès
2014-01-15	Christmas is over...	Maxime Dénès
2013-12-17	Tentative fix of the guardedness checker by Christine and me. All stdlib and ...	Matthieu Sozeau
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	Turn many List.assoc into List.assoc_f	letouzey
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-05-14	Delayed the computation of parameters in sort polymorphism of	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-19	Array.create is deprecated	pboutill
2012-12-14	Modulification of identifier	ppedrot
2012-11-22	Monomorphization (kernel)	ppedrot
2012-11-13	More monomorphizations	ppedrot
2012-11-08	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot
2012-09-14	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	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-03-02	Noise for nothing	pboutill
2011-10-05	It happens that the type inference algorithm (pretyping) did not check	herbelin
2011-07-04	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey
2010-12-18	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-03	"Improved" the form of the inferred type of "match" by	herbelin
2010-05-20	fixed guard check with commutative cuts	barras
2010-05-18	Applicative commutative cuts in Fixpoint guard condition	pboutill
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-03-12	fixed confusion between number of cstr arguments and number of pattern variab...	barras
2010-03-11	introduced lazy computation of size info in the guard condition	barras
2009-12-07	revert on commit r12553	barras
2009-12-01	two improvements of the guard condition:	barras
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-11	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin