coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	changement type_var et signature	filliatr	2001-03-28
*	amelioration de la structure des univers	barras	2001-03-28
*	conservation des arguments dans Prop (snif)	filliatr	2001-03-27
*	extraction recursive d'un morceau d'environnement	filliatr	2001-03-27
*	trace des inductifs sur Prop	letouzey	2001-03-27
*	cache pour les constantes	filliatr	2001-03-26
*	eta-expansion des constructeurs si necessaire (a posteriori en miniML)	filliatr	2001-03-23
*	suppression des param dans inductifs. suite du Cases	letouzey	2001-03-23
*	Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les branch...	letouzey	2001-03-21
*	affichage declarations fix + bug extraction sumbool_rec mis a jour	filliatr	2001-03-20
*	mlutil	filliatr	2001-03-20
*	extraction naive de fix et case	filliatr	2001-03-20