coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards.	herbelin	2008-03-23
*	Une passe sur les réels:	herbelin	2008-03-23
*	CoqIDE default font set to monospace so as indentation to be meaningful	herbelin	2008-03-23
*	Compatibility fixes, backtrack on definitions of reflexive,	msozeau	2008-03-22
*	One more AVL reorganisation: separate pure functions from proofs + functional...	letouzey	2008-03-21
*	Correct bug introduced in r10589, where we lost information that	msozeau	2008-03-21
*	Some "if then else" instead of orb and andb, in order to vm_compute lazily	letouzey	2008-03-21
*	Add a flag to control rewriting under lambdas. Otherwise makes some	msozeau	2008-03-20
*	Installation des .vo nécessaire à BigQ	notin	2008-03-20
*	Correction d'un bug sur les modules de la forme:	soubiran	2008-03-20
*	still some useless invariants in FSetAVL	letouzey	2008-03-20
*	some references to IntMap forgotten in last commit	letouzey	2008-03-19
*	migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...	letouzey	2008-03-19
*	Coq.Relations.Relations can move back to its short name	letouzey	2008-03-19
*	Do another pass on the typeclasses code. Correct globalization of class	msozeau	2008-03-19
*	tactique gappa	filliatr	2008-03-19
*	Various improvements of coqdep, resulting in a big speedup	letouzey	2008-03-19
*	Implementation of rewriting under lambdas. Tested on exists only.	msozeau	2008-03-18
*	Added a function to rebuild an elim scheme from elim_scheme_info. Will	courtieu	2008-03-18
*	Hint for Debian users.	glondu	2008-03-18
*	improved the implementation of rtree	barras	2008-03-18
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10690 85f007b7-540e-0...	barras	2008-03-18
*	Correct implementation of normalization of signatures using setoid	msozeau	2008-03-18
*	* Small change in the make_eq_decidability call : the functions does not (yet)	vsiles	2008-03-18
*	Add the possibility of specifying constants to unfold for typeclass	msozeau	2008-03-17
*	* Factorizing code : context_chop was used in several files (even as chop_con...	vsiles	2008-03-17
*	Removed unneeded tactics from RelationClasses. Use	msozeau	2008-03-16
*	Using the "relation" constant made some unifications fail in the new	msozeau	2008-03-16
*	Ajout cible programs comme synonyme de subtac	herbelin	2008-03-16
*	Misc: Add test for bug 1704, now closed. Add usual syntax for lists in	msozeau	2008-03-16
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
*	Minor fixes on setoid rewriting. Now uses definitions of [relation] and	msozeau	2008-03-16
*	Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)	letouzey	2008-03-15
*	Forgot the test file.	msozeau	2008-03-15
*	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau	2008-03-15
*	Adapt funind to the RLetPattern constructor.	msozeau	2008-03-15
*	Backtrack sur le test censé discriminer entre une erreur d'evar non	herbelin	2008-03-15
*	Application de refresh_universes dans typing.ml et retyping.ml : les	herbelin	2008-03-15
*	Suppress some warnings by writing ugly Coq.Relations.Relations in some .v	letouzey	2008-03-14
*	avoid universe problems with pf_get_type in f_equal	letouzey	2008-03-14
*	New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefile	letouzey	2008-03-14
*	Backtrack wrong commit.	courtieu	2008-03-14
*	kill a warning (and clean the code around)	letouzey	2008-03-14
*	nettoyage de code obsolete.	soubiran	2008-03-14
*	Ajout des alias de module dans le noyau.	soubiran	2008-03-14
*	tactique gappa	filliatr	2008-03-14
*	indentation.	courtieu	2008-03-14
*	fix the 'decreasing on Xth' message	letouzey	2008-03-13
*	trying f	courtieu	2008-03-13
*	* Catching a Not_found exception when trying to use Scheme Equality	vsiles	2008-03-12