coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin	2009-08-11
*	Ajout des .annot dans le .gitignore.	aspiwack	2009-08-11
*	Fixed extra space in printing notation { x & P } + minor other things	herbelin	2009-08-11
*	Infix (r12268 continued)	herbelin	2009-08-11
*	Add support for "Infix ... := constr" instead of just "Infix ... := ref".	herbelin	2009-08-11
*	Relatively ad hoc fix to an ill-typed instantiation bug in type	herbelin	2009-08-11
*	Fixed incorrect optimization in Prettyp.pr_located_qualid introduced	herbelin	2009-08-07
*	Cleaning of Nametab continued + fixed a compilation bug in previous commit.	herbelin	2009-08-06
*	- Cleaning phase of the interfaces of libnames.ml and nametab.ml	herbelin	2009-08-06
*	Move out JMeq of subst for compatibility (it affects e.g. the	herbelin	2009-08-06
*	changed deprecated setoid into relation	amahboub	2009-08-05
*	- Add more precise error localisation when one of the application fails	herbelin	2009-08-04
*	Fixed subst failing when a truly heterogeneous JMeq hyp is in the	herbelin	2009-08-04
*	Added "etransitivity".	herbelin	2009-08-03
*	Improved parameterization of Coq:	herbelin	2009-08-02
*	Fixed a typo in "info" for tactic "right".	herbelin	2009-08-02
*	csdpcert + unix	fbesson	2009-08-01
*	addition of lia.cache - csdp.cache is now handled by micromega not csdpcert	fbesson	2009-07-31
*	micromega : Better parsing of formulae - smaller proof terms for Z - redesign...	fbesson	2009-07-30
*	psatz Z -> psatz Z 1	fbesson	2009-07-30
*	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