coq - The formal proof system

Age	Commit message (Expand)	Author
2008-07-26	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin
2008-07-25	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-24	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-23	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-22	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-21	Suite commit 11236	notin
2008-07-20	Extraction: better dependency computation (after optimisations)	letouzey
2008-07-18	- 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-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