coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-04	add the compilation of the files needed for the interface with pcoq.	bertot
2001-04-04	adding entry points for the arguments of the Comment command.	bertot
2001-04-04	Adding A command for comments, this makes it possible to have structured	bertot
2001-04-04	dependencies required for contrib/interface	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	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