coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...	notin	2008-07-07
*	Micromega: doc + test-suite update	fbesson	2008-07-07
*	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau	2008-07-07
*	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey	2008-07-04
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	Prise en compte de changments dans subtac	notin	2008-07-03
*	Stop using the discrimination net in typeclasses/setoid rewrite, which was	msozeau	2008-07-02
*	Correct a bug in the coercion code where we did not go under constants	msozeau	2008-07-02
*	Improved robustness of micromega parser. Proof search of Micromega test-suite...	fbesson	2008-07-02
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	Various bug fixes in type classes and subtac:	msozeau	2008-07-01
*	correction sur la doc des modules	soubiran	2008-07-01
*	Encore une suite au 11188/11193 (c'était pas un bon jour)	herbelin	2008-07-01
*	QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...	letouzey	2008-06-30
*	Fichiers oubliés lors du 11188 :-(	herbelin	2008-06-30