coq - The formal proof system

Age	Commit message (Expand)	Author
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-17	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-16	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-15	Autour du parsing:	herbelin
2008-07-15	Tentative de relecture des scripts de Mult.v au regard des tactiques actuelles	herbelin
2008-07-13	update doc Micromega	fbesson
2008-07-11	Correction d'un autre bug autour de la gestion des niveaux vides de	herbelin
2008-07-10	Bug résiduel du backtrack de coqide se produisant lorsque la limite de	herbelin
2008-07-09	Documentation fixes.	msozeau
2008-07-09	test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq	letouzey
2008-07-08	forgotten debug printf in coqmktop (anyway, can be obtained by -echo)	letouzey
2008-07-08	Suite de la révision #11212	notin
2008-07-07	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-04	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey
2008-07-04	Fixes in handling of implicit arguments:	msozeau
2008-07-03	Prise en compte de changments dans subtac	notin
2008-07-02	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-01	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-06-30	QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...	letouzey
2008-06-30	Fichiers oubliés lors du 11188 :-(	herbelin
2008-06-29	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-28	QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...	letouzey
2008-06-27	(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-26	Mauvaise dépendance dans Makefile.doc	notin
2008-06-26	Oubli lors de la révision #11177	notin
2008-06-25	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