coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-20	Ajout des entetes	delahaye
2001-04-20	nettoyage	filliatr
2001-04-19	Add a treatement of elaborate Intros tactics, CONJPATTERN and family.	bertot
2001-04-19	scripts; extraction False_rec	filliatr
2001-04-19	blindage False_rec	filliatr
2001-04-19	cofix; axiomes; eta-expansions pour variables de types mal generalisees (en c...	filliatr
2001-04-19	ZArith --> Zarith	mohring
2001-04-19	synchonization des tables d'extraction	filliatr
2001-04-19	remplace Zarith par ZArith	mohring
2001-04-19	modifs des scripts de test auto	filliatr
2001-04-19	deplacement de l'optimisation inductif singleton	letouzey
2001-04-19	script de bench automatique pour extraction	letouzey
2001-04-19	Making sure there will be no warnings at compile time.	bertot
2001-04-19	Ajout de Field	delahaye
2001-04-18	Correcting a problem of s that appears behind a Let when there are	bertot
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-13	eliminiation des singletons du genre sig + divers	letouzey
2001-04-12	nouvelle gestion des variables de type ML	letouzey
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-10	bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app	letouzey
2001-04-10	portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega	filliatr
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-09	exemples Correctness	filliatr
2001-04-09	branchement extraction en standard (pas de Require)	filliatr
2001-04-09	réparation Quote	filliatr
2001-04-08	Ajout lemmes arithmetiques	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-05	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr
2001-04-04	axiomes dans les types	filliatr
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-04-04	implification de extract_constr et extract_term	letouzey
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
2001-04-04	Files that handle the dialogue with the graphical user-interface pcoq.	bertot
2001-04-04	documentation	filliatr
2001-04-04	supression vieux fichiers extraction	filliatr
2001-04-04	rollback sur les commandes Extract Constant/Inductive; nettoyage et documenta...	filliatr
2001-04-04	deux fichiers (past et ptype) uniquement sous forme de .mli	filliatr
2001-04-03	commandes Extract Constant/Inductive; message d'erreur pour les axiomes	filliatr
2001-04-03	ménage	filliatr
2001-04-03	psyntax.ml4 sous CVS	filliatr
2001-04-03	utilisation de Options.if_verbose	filliatr
2001-04-02	parenthèses autour des types dans les arguments des constructeurs	filliatr
2001-04-02	underscores pour les variables représentant des propositions	filliatr