coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	The function filter_by_module, that was previously exported was not the	bertot	2001-04-03
*	Export a function (build_inductive) that is used in the graphical interface.	bertot	2001-04-03
*	Make sure that the COQTOP variable is really used, when it is set.	bertot	2001-04-03
*	Make it possible to perform proofs by induction even on non-inductive types,	bertot	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
*	installation des .cmo pour l'extraction	filliatr	2001-04-03
*	mise a jour pour ocamlweb	filliatr	2001-04-02
*	mise a jour	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	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
*	bug Fix signalé par Alexandre (even/odd mal interprété)	filliatr	2001-04-02
*	branchement extraction (bytecode seulement)	filliatr	2001-03-30
*	Ajout de lemmes sur les booleens	mohring	2001-03-30
*	Introduction d'une preuve de False_rec	mohring	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
*	deux fois $Id$	filliatr	2001-03-29
*	fichiers extraction	filliatr	2001-03-29
*	changement type_var et signature	filliatr	2001-03-28
*	amelioration de la structure des univers	barras	2001-03-28
*	Interprétation des qualidarg	herbelin	2001-03-27
*	conservation des arguments dans Prop (snif)	filliatr	2001-03-27
*	mise a jour	filliatr	2001-03-27
*	extraction recursive d'un morceau d'environnement	filliatr	2001-03-27
*	trace des inductifs sur Prop	letouzey	2001-03-27
*	Bibliotheque Num	mohring	2001-03-26
*	cache pour les constantes	filliatr	2001-03-26
*	ocaml 3.01 requis	herbelin	2001-03-25
*	Tag pour une beta3-ocaml3.01	herbelin	2001-03-25
*	MAJ	herbelin	2001-03-23
*	MAJ	herbelin	2001-03-23
*	Les règles d'affichage ajoutés dans le commit précédent avait le même no...	herbelin	2001-03-23
*	amelioration de la consommation memoire de la conversion en eta-expansant	barras	2001-03-23
*	mise a jour	filliatr	2001-03-23
*	eta-expansion des constructeurs si necessaire (a posteriori en miniML)	filliatr	2001-03-23
*	La strategie de recherche de lookup_eliminator etait insuffisante	herbelin	2001-03-23
*	suppression des param dans inductifs. suite du Cases	letouzey	2001-03-23