coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-30	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin
2004-03-30	Fabrication de l'uri a partir du path utilisateur	herbelin
2004-03-29	Retrait debogage	herbelin
2004-03-29	Export du type de preuve en cours pour xml	herbelin
2004-03-29	Debug prints removed.	sacerdot
2004-03-29	Export Require	herbelin
2004-03-27	Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; divers	herbelin
2004-03-27	-dead code removed.	sacerdot
2004-03-26	Theory file for file A.B.C.v is put in A/B/C.theory.xml.	sacerdot
2004-03-26	Ajout exportation des 'theory.xml' + divers	herbelin
2004-03-25	The DTD that describes the CIC (with Explicit Named Substitutions) format.	sacerdot
2004-03-25	Fix and Cofix blocks with mutually defined functions having the same	sacerdot
2004-03-25	me = andouille	letouzey
2004-03-25	Selon les optims, le let-in peut avoir maintenant des args	letouzey
2004-03-25	Updated.	sacerdot
2004-03-25	ProofTree2Xml is no longer directly used by Xmlcommand.	sacerdot
2004-03-25	No longer used.	sacerdot
2004-03-25	Dead code removed.	sacerdot
2004-03-25	Comment removed.	sacerdot
2004-03-24	MAJ Claudio pour v8	herbelin
2004-03-24	Reparation typo de HH dans MAJ de Claudio	herbelin
2004-03-24	MAJ Claudio pour v8	herbelin
2004-03-24	Utilisation du printer approprie a la version de syntaxe	herbelin
2004-03-24	Nettoyage	herbelin
2004-03-24	Effacement tardif de ce fichier qui a ete transforme le 5 nov 2002 en une ver...	herbelin
2004-03-24	nouvelle commande Set Extraction Flag: reglage fins des optims	letouzey
2004-03-23	meme correction de bug, en moins bourrin	letouzey
2004-03-22	PolyList -> List	letouzey
2004-03-22	correction d'un bug faisant inliner minus, mult, ...	letouzey
2004-03-20	petit rajeunissement du test d'extraction	letouzey
2004-03-15	preparation pour release (suite)	barras
2004-03-15	To make that the translation process does not fail on data produced by	bertot
2004-03-15	oops	corbinea
2004-03-14	minor changes	corbinea
2004-03-14	congruence now handles disequalities	corbinea
2004-03-13	Mise en place temporaire d'un afficheur de 'language' pour le traducteur	herbelin
2004-03-11	Ooops ! bug in firstorder fixed (let's hope no one noticed)	corbinea
2004-03-11	reals: renamed type option into field_rel_option	marche
2004-03-05	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras
2004-03-04	Reparation ROmega V8/Omega ZERO/POS/NEG	mohring
2004-03-03	adaptation V8 version Pierre Cregut	mohring
2004-03-03	takes better account of the new possibility to pass a parametric count argument	bertot
2004-03-03	removes capital letters in two tactic names.	bertot
2004-03-03	make sure the implicit argument indications are in the right order	bertot
2004-03-02	Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les no...	herbelin
2004-03-02	Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...	herbelin
2004-03-01	code mort	herbelin
2004-03-01	Ajout IntroPattern comme type d'argument générique	herbelin
2004-03-01	Protection d'un 'clear' qui peut etre dependant	herbelin
2004-02-26	Keep structure information for Fixpoint declaration and Fix terms	bertot