coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	More monomorphizations	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	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-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24