coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Relax a bit the guard condition.	Maxime Dénès	2014-08-06
*	One more optimization for guard checking of cofixpoints.	Maxime Dénès	2014-08-04
*	More optimization in guard checking.	Maxime Dénès	2014-08-04
*	Fix an exponential behavior in guard checker for cofixpoints.	Maxime Dénès	2014-08-04
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Optimize check of new subterm relation on match.	Maxime Dénès	2014-07-31
*	Fix dynamic computation of recargs for mutual inductives.	Maxime Dénès	2014-07-31
*	Minor cleaning.	Maxime Dénès	2014-07-22
*	Revert "Extend subterm relation to pattern matching in return predicates."	Maxime Dénès	2014-07-22
*	Revert "Propagate size info through pattern matching in predicates, for the"	Maxime Dénès	2014-07-22
*	Propagate size info through pattern matching in predicates, for the	Maxime Dénès	2014-07-22
*	Extend subterm relation to pattern matching in return predicates.	Maxime Dénès	2014-07-22
*	Fix check_inductive_codomain.	Maxime Dénès	2014-07-22
*	Refine check_is_subterm.	Maxime Dénès	2014-07-22
*	Refined guard condition of cofixpoints, to anticipate potential futur	Maxime Dénès	2014-07-22
*	First attempt at a fix for guard condition on cofixpoints.	Maxime Dénès	2014-07-22
*	Typo in comment.	Maxime Dénès	2014-07-22
*	Made intersection on regular trees less intensional.	Maxime Dénès	2014-07-22
*	Refining match subterm and commutative cut rules. The parameters that are	Maxime Dénès	2014-07-22
*	Tentative fix for the commutative cut subterm rule.	Maxime Dénès	2014-07-22
*	Tentative patch for incompatibility between subterm relation and dependent	Maxime Dénès	2014-07-22
*	Removing dead code.	Pierre-Marie Pédrot	2014-06-17
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Reuse universe level substitutions for template polymorphism, fixing performance	Matthieu Sozeau	2014-05-09
*	Avoid allocations in type_of_inductive	Matthieu Sozeau	2014-05-08
*	- 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-05-06
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	Fix guard condition for nested cofixpoints.	Maxime Dénès	2014-04-10
*	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
*	Tentative fix of the guardedness checker by Christine and me. All stdlib and ...	Matthieu Sozeau	2013-12-17
*	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-10-24
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (kernel)	ppedrot	2012-11-22