coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Hipattern: two generic equalities on constr spotted & rewritten	puech	2011-07-29
*	Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...	herbelin	2011-07-16
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fixed subst failing when a truly heterogeneous JMeq hyp is in the	herbelin	2009-08-04
*	Added "etransitivity".	herbelin	2009-08-03
*	- Allowing multiple calls to tactic fix with automatic generation of	herbelin	2009-05-17
*	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin	2008-12-31
*	- Fixed bugs and compatibilities issues in	herbelin	2008-12-30
*	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin	2008-12-28
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
*	- Fixed minor bug #1994 in the tactic chapter of the manual [doc]	herbelin	2008-11-22
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22