coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)	herbelin	2008-06-21
*	Various improvements in handling of evars in general and typing	msozeau	2008-06-21
*	typo in a comment	letouzey	2008-06-20
*	Little fixes: print unbound variable in error message (patch by Samuel	msozeau	2008-06-19
*	incomplete bugfix for info	corbinea	2008-06-19
*	removed unwanted linebreaks in pretty printing	corbinea	2008-06-19
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	Fix bug in implementation of splitting of class constraints.	msozeau	2008-06-18