coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Correction d'un bug dans l'analyse des contraintes non résolues	herbelin	2008-06-29
*	Correction bug "parser" suite changement syntaxe	herbelin	2008-06-29
*	Lissage de la gestion des chemins de chargement de fichiers :	herbelin	2008-06-29
*	Préférence donnée aux constantes qui ne sont pas des projections	herbelin	2008-06-29
*	QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...	letouzey	2008-06-28
*	(Partial) fix for bug #1892, adding a missing newline.	msozeau	2008-06-27
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	Changement de catch_error pour qu'il rattrape les erreurs d'arguments	aspiwack	2008-06-27
*	Logo Coq dans coqide	notin	2008-06-27
*	Mauvaise dépendance dans Makefile.doc	notin	2008-06-26
*	Oubli lors de la révision #11177	notin	2008-06-26
*	Some work on BigQ :	letouzey	2008-06-25
*	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin	2008-06-25
*	Report de la révision #11175 de la branche v8.2 vers le trunk	notin	2008-06-25
*	Installation de la documentation	notin	2008-06-25
*	Micromega : bugs fixes - renaming of tactics - documentation	fbesson	2008-06-25
*	Typo in documentation (isn't it?)	glondu	2008-06-25
*	Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...	soubiran	2008-06-25
*	Catch a Not_found exception in the Combined Scheme mechanism to hide an ugly	vsiles	2008-06-24
*	Suppression de l'option -dump-glob et ajout d'une option -no-glob	notin	2008-06-24
*	MAJ fichiers spécifiques trunk	herbelin	2008-06-22
*	Rename obligations_tactic to obligation_tactic and fix bugs #1893.	msozeau	2008-06-22
*	Code cleanup in typeclasses, remove dead and duplicated code.	msozeau	2008-06-21
*	Correction petit bug sur révision 11159 (res_pf fait un effet de bord	herbelin	2008-06-21
*	Fix bug #1889, correct globalization in class declarations.	msozeau	2008-06-21