coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega	filliatr	2001-04-10
*	Modified searchPattern. Before this correction, constructors were overlooked,	bertot	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-10
*	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-09
*	Ajout lemmes arithmetiques	mohring	2001-04-08
*	ajout des lemmes Zimmerman	mohring	2001-04-08
*	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-07
*	correction d'un bug de Quote	filliatr	2001-04-06
*	bug Print Proof; usage coqtop/coqc	filliatr	2001-04-06
*	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr	2001-04-05
*	array_fold_left_i	filliatr	2001-04-05
*	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-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