coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-07	Two constants had been given in the wrong package (Logic_type instead of	bertot
2001-04-06	correction d'un bug de Quote	filliatr
2001-04-06	bug Print Proof; usage coqtop/coqc	filliatr
2001-04-05	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr
2001-04-05	array_fold_left_i	filliatr
2001-04-04	axiomes dans les types	filliatr
2001-04-04	ajout de coq_example# dans coq-tex	werner
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-04-04	Adding the dependencies for the parser that is used in the interface pcoq.	bertot
2001-04-04	implification de extract_constr et extract_term	letouzey
2001-04-04	adding the directives to compile the parser that is used in the graphical	bertot
2001-04-04	Added a flag that makes it possible to re-load files while taking only the	bertot
2001-04-04	Added two files that are used for the connection with the graphical user-inte...	bertot
2001-04-04	Add a flag to avoid sending too many warnings when reloading syntax files	bertot
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	Add a Comments command, that does nothing, but is quite useful to to have	bertot
2001-04-04	add the binary coq-interface, used for the communication with the graphical	bertot
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