coq - The formal proof system

Age	Commit message (Expand)	Author
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
2001-04-06	correction d'un bug de Quote	filliatr
2001-04-06	bug Print Proof; usage coqtop/coqc	filliatr
2001-04-05	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr
2001-04-05	array_fold_left_i	filliatr
2001-04-04	axiomes dans les types	filliatr
2001-04-04	ajout de coq_example# dans coq-tex	werner
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-04-04	Adding the dependencies for the parser that is used in the interface pcoq.	bertot
2001-04-04	implification de extract_constr et extract_term	letouzey
2001-04-04	adding the directives to compile the parser that is used in the graphical	bertot
2001-04-04	Added a flag that makes it possible to re-load files while taking only the	bertot
2001-04-04	Added two files that are used for the connection with the graphical user-inte...	bertot
2001-04-04	Add a flag to avoid sending too many warnings when reloading syntax files	bertot
2001-04-04	These files are used to construct an independent parser, that is a small	bertot
2001-04-04	These files are loaded coq-interface to make a process that is "pcoq" enabled.	bertot
2001-04-04	Make sure the constructors of Z and positive are recognized: they show up	bertot