coq - The formal proof system

Age	Commit message (Expand)	Author
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	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-02	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-03-30	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-29	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-28	changement type_var et signature	filliatr
2001-03-28	amelioration de la structure des univers	barras
2001-03-27	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-26	Bibliotheque Num	mohring
2001-03-26	cache pour les constantes	filliatr
2001-03-25	ocaml 3.01 requis	herbelin
2001-03-25	Tag pour une beta3-ocaml3.01	herbelin
2001-03-23	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-22	Règle de syntaxe pour CASTEDCOMMAND	herbelin