coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Git ignore files	herbelin	2009-07-30
*	For git users, a global .gitignore file	letouzey	2009-07-30
*	OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith	letouzey	2009-07-24
*	List: add a iff-based lemma about In and ++	letouzey	2009-07-24
*	Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"	letouzey	2009-07-24
*	Better comparison functions in OrderedTypeEx	letouzey	2009-07-22
*	Use unfold directly in unfold_equations. Fixes test-suite.	msozeau	2009-07-20
*	Use camlp4 to accept some specific non-exhaustive patterns in groebner	letouzey	2009-07-20
*	Move some examples for groebner into a test-suite file	letouzey	2009-07-20
*	Typo in a comment	letouzey	2009-07-20
*	- Granted wish #2138 (support for local binders in syntax of Record fields).	herbelin	2009-07-15
*	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin	2009-07-15
*	Simplify eauto and fix it for compatibility, allowing full delta during	msozeau	2009-07-14
*	Use the proper unification flags in e_exact. This makes exact fail a bit	msozeau	2009-07-09
*	Allow coqdoc comments inside definition bodies.	msozeau	2009-07-09
*	Correction bug 2134.	soubiran	2009-07-09
*	Fixed bug #2116 ("simpl" created ill-typed term while accepting	herbelin	2009-07-08
*	Don't use recent ocaml tolerance for pattern "ProjectVar _" when	herbelin	2009-07-08
*	Simplify addition of hints to a hint_db. Rebuild the dnet associated	msozeau	2009-07-08
*	Use user-given implicits from the arity in inductive definitions.	msozeau	2009-07-08
*	Reactivation of pattern unification of evars in apply unification, in	herbelin	2009-07-08
*	Add heuristic based on non-linearity of evars to determine whether an	herbelin	2009-07-08
*	Fixed anomaly when trying to load non existing file starting with "./" or "../".	herbelin	2009-07-08
*	Fixing bug 2129 (evar introduced to remember an ambiguous projection	herbelin	2009-07-08
*	Completing support for F5=About by adding About to the state-preserving comma...	herbelin	2009-07-08
*	Jolification : tentative de supprimer les "( evd)" et associés qui	aspiwack	2009-07-07
*	change in the order of unification constraints solving (for canonical structu...	amahboub	2009-07-06
*	repport of commit r12221	jforest	2009-07-04
*	Support for binding Coq root read-only in -R option	herbelin	2009-07-01
*	Add new variants of [rewrite] and [autorewrite] which differ in the	msozeau	2009-06-30
*	Miscellaneous practical commits:	herbelin	2009-06-29
*	Fix bug introduced by last revision, subtac_cases was returning the	msozeau	2009-06-29
*	Raise an error and not an anomaly if a rewrite is attempted on a	msozeau	2009-06-28
*	Abstract the tycon by the matched terms when turning them into variables	msozeau	2009-06-28
*	Improve return predicate inference by making the return type dependent	msozeau	2009-06-28
*	propagation sur le trunk du commit 12101	soubiran	2009-06-26
*	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau	2009-06-26
*	Correct treatment of dependent products in signatures: create the evars	msozeau	2009-06-22
*	Fixes for r12197, the refined evars were not returned in case fail_evar	msozeau	2009-06-22
*	documented a bug of pattern unification with metas	barras	2009-06-22
*	made several occurrences of (eapply ...; eauto) not rely on the lack of patte...	barras	2009-06-22
*	Report de la révision #12200 (bug #2125)	notin	2009-06-22
*	remove some unused functions (which are part of a soon-to-be obsolete	vgross	2009-06-22
*	clearing unused functions	vgross	2009-06-22
*	Use more consistent resolution parameters in Program and regular typing	msozeau	2009-06-18
*	Fix "unsatisfiable constraints" error messages to include all the	msozeau	2009-06-18
*	Try typeclass resolution in coercion if no solution can be found to a	msozeau	2009-06-18
*	Fallback on not using [fix_proto] if the right imports aren't there, the	msozeau	2009-06-17
*	Reimplementation of leibniz rewrite to control the instantiation of the	msozeau	2009-06-16
*	Allow anonymous instances again, with syntax [Instance: T] where T	msozeau	2009-06-15