coq - The formal proof system

Age	Commit message (Expand)	Author
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	Mise a jour de la config pour distrib	mohring
2001-04-10	MAJ	herbelin
2001-04-10	Bug affichage LETPATTERN	herbelin
2001-04-10	Bug context incoherent au passage du lambda et du let dans evar_eqappr	herbelin
2001-04-09	Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal	herbelin
2001-04-09	Uniformisation des 'Save def_tok id'	herbelin
2001-04-09	nettoyage d'entrees de grammaires inutiles	courant
2001-04-09	exemples Correctness	filliatr
2001-04-09	branchement extraction en standard (pas de Require)	filliatr
2001-04-09	mise à jour	filliatr
2001-04-09	réparation Quote	filliatr
2001-04-09	MAJ	herbelin
2001-04-08	Ajout lemmes arithmetiques	mohring
2001-04-08	ajout des lemmes Zimmerman	mohring
2001-04-07	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-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