coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	(Partially) Revert previous commit because of FTBFS	glondu	2008-07-27
*	Add -browser option to configure script	glondu	2008-07-27
*	Oups (on refait le 11268 en mieux)	herbelin	2008-07-27
*	Even better test for choosing rewrite or setoid_rewrite.	msozeau	2008-07-26
*	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin	2008-07-26
*	Suite 11266 (warning tools/gallina.ml)	herbelin	2008-07-25
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	Fixed bug #1904 (instances of evars were no longer substituted since	herbelin	2008-07-25
*	A better test for relations being setoids or not: do leibniz rewrite iff	msozeau	2008-07-25
*	More compatibility fixes, revert the tauto fix that prevented	msozeau	2008-07-25
*	Tauto breaking not only binary "conjunctions" seems like a bad idea	msozeau	2008-07-24
*	A (safe) implementation of prolog's cut in the typeclasses eauto to avoid	msozeau	2008-07-24
*	Fix bug #1913, checking for unresolved evars which aren't obligations.	msozeau	2008-07-24
*	fixed loop in dependency fold of the checker	barras	2008-07-24
*	moved magic numbers to configure (share coq/coqchk)	barras	2008-07-24
*	broke cyclic dependencies	barras	2008-07-24
*	Suite commit 11236	notin	2008-07-24
*	Propagation de l'information "strict" (càd à toplevel ou en train de	herbelin	2008-07-24
*	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin	2008-07-23
*	Stop glob messages to be printed by default on stdout	letouzey	2008-07-23
*	Oops... forgot some debug code.	msozeau	2008-07-23
*	Add test-suite file for bug# 1905 and minor fix in Program/Equality.	msozeau	2008-07-22
*	New tactics [conv] to test convertibility (actually, unification) of two	msozeau	2008-07-22
*	A try at allowing matching on applications as a binary syntax node by default.	msozeau	2008-07-22
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Oubli lors du commit #11236	notin	2008-07-22
*	Suite commit 11236	notin	2008-07-21
*	Extraction: better dependency computation (after optimisations)	letouzey	2008-07-20
*	- Rebranchement backtrack du langage déclaratif dans Coqide	herbelin	2008-07-18
*	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin	2008-07-18
*	Modification rapide du message d'erreur lorsqu'un _ ne peut être	herbelin	2008-07-18
*	Affichage intempestif d'information de globalisation + numéro de version dan...	notin	2008-07-18
*	fixed indentation of subgoals for Show Script	barras	2008-07-17
*	- Suppression de Rstar/Newman peu utilisables comme biblio (encodage	herbelin	2008-07-17
*	- coqdoc: correction d'un bug sur les commentaires imbriqués	notin	2008-07-17
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Ajout de cibles pour le manuel de référence (refman-nodep, stdlib-nodep, re...	notin	2008-07-16
*	ROmega : make it work even if no Require Import ZArith has been done	letouzey	2008-07-16
*	Ajout d'une option pour contrôler l'installation automatique de la documenta...	notin	2008-07-16
*	Quelques modifications autour du filtrage Ltac:	herbelin	2008-07-16
*	Autour du parsing:	herbelin	2008-07-15
*	Tentative de relecture des scripts de Mult.v au regard des tactiques actuelles	herbelin	2008-07-15
*	update doc Micromega	fbesson	2008-07-13
*	Correction d'un autre bug autour de la gestion des niveaux vides de	herbelin	2008-07-11
*	Bug résiduel du backtrack de coqide se produisant lorsque la limite de	herbelin	2008-07-10
*	Documentation fixes.	msozeau	2008-07-09
*	test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq	letouzey	2008-07-09
*	forgotten debug printf in coqmktop (anyway, can be obtained by -echo)	letouzey	2008-07-08
*	Suite de la révision #11212	notin	2008-07-08
*	Fix implicit arguments in sections bug and check for resolution of evars when	msozeau	2008-07-07