coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-19
*	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-18
*	eliminiation des singletons du genre sig + divers	letouzey	2001-04-13
*	nouvelle gestion des variables de type ML	letouzey	2001-04-12
*	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 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-10
*	exemples Correctness	filliatr	2001-04-09
*	branchement extraction en standard (pas de Require)	filliatr	2001-04-09
*	réparation Quote	filliatr	2001-04-09
*	Ajout lemmes arithmetiques	mohring	2001-04-08
*	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-07
*	correction d'un bug de Quote	filliatr	2001-04-06
*	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr	2001-04-05
*	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-04
*	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-03
*	parenthèses autour des types dans les arguments des constructeurs	filliatr	2001-04-02
*	underscores pour les variables représentant des propositions	filliatr	2001-04-02
*	inductifs vides	filliatr	2001-04-02
*	ml_pop au lieu de ml_lift dans betared_ast	filliatr	2001-04-02
*	à faire	filliatr	2001-04-02
*	branchement extraction (bytecode seulement)	filliatr	2001-03-30
*	extraction modulaire	filliatr	2001-03-30
*	extraction modulaire + environnement des Fix corrigé	filliatr	2001-03-30
*	repertoire pour les tests d'extraction	filliatr	2001-03-30
*	application avec bcp args	letouzey	2001-03-30
*	beta-reduction	filliatr	2001-03-30
*	mise en place de Correctness (ne compile pas encore)	filliatr	2001-03-29