coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-18	Correcting a problem of s that appears behind a Let when there are	bertot
2001-04-18	there was a wrong order in the previous version. One was trying to	bertot
2001-04-18	Make sure the binaries needed for pcoq are compiled by default.	bertot
2001-04-18	Erreur Makefile JMeq	mohring
2001-04-18	Changing the commands to switch to textual explanation of proofs.	bertot
2001-04-18	Adding files for the production of textual explanations as used in pcoq.	bertot
2001-04-16	* empty log message *	courant
2001-04-15	MAJ	herbelin
2001-04-15	Mise en page	herbelin
2001-04-15	to_constr renvoie directement un constr pour contourner l'ancien Term.mk_cons...	herbelin
2001-04-15	Suppression de mk_constr qui ne respectait pas l'invariant des applications (...	herbelin
2001-04-15	Bug affichage d'implicites pour les vars liees	herbelin
2001-04-15	Bug affichage ordre des variables d'un pattern	herbelin
2001-04-14	Reparation du bug de Try	delahaye
2001-04-14	Non parenthesage des applications de tactiques	delahaye
2001-04-13	Mise en place d'un test de clauses non utilisees	herbelin
2001-04-13	Reparation de l'affichage des THEN's	delahaye
2001-04-13	eliminiation des singletons du genre sig + divers	letouzey
2001-04-13	ajout de tests	mohring
2001-04-13	MAJ	herbelin
2001-04-12	Ajout de _ dans les patterns d'intro	mohring
2001-04-12	nouvelle gestion des variables de type ML	letouzey
2001-04-12	Mis un message d'erreur explicite pour l'echec de Elim en cas	mohring
2001-04-12	Ajout de l'egalite de John Major	mohring
2001-04-11	coqweb	filliatr
2001-04-11	documentation automatique de la bibliothèque standard	filliatr
2001-04-11	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...	filliatr
2001-04-11	Bug rapporte par Randy en Mars 2000	herbelin
2001-04-10	bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app	letouzey
2001-04-10	-I contrib/extraction pour compiler Extraction.v	filliatr
2001-04-10	portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega	filliatr
2001-04-10	Modified searchPattern. Before this correction, constructors were overlooked,	bertot
2001-04-10	réparation Correctness; options Extraction (changement de syntaxe)	filliatr
2001-04-10	bug lift dans IsRel de extract_type. Axiomes dans extract_type	letouzey
2001-04-10	Mise a jour de la config pour distrib	mohring
2001-04-10	MAJ	herbelin
2001-04-10	Bug affichage LETPATTERN	herbelin
2001-04-10	Bug context incoherent au passage du lambda et du let dans evar_eqappr	herbelin
2001-04-09	Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal	herbelin
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-09	nettoyage d'entrees de grammaires inutiles	courant
2001-04-09	exemples Correctness	filliatr
2001-04-09	branchement extraction en standard (pas de Require)	filliatr
2001-04-09	mise à jour	filliatr
2001-04-09	réparation Quote	filliatr
2001-04-09	MAJ	herbelin
2001-04-08	Ajout lemmes arithmetiques	mohring
2001-04-08	ajout des lemmes Zimmerman	mohring
2001-04-07	Make sure the parser knows about the constructors of type nat, so	bertot
2001-04-07	Two constants had been given in the wrong package (Logic_type instead of	bertot