coq - The formal proof system

Age	Commit message (Expand)	Author
2001-04-24	Fin d'optimisation (cas modules) + warning pour coind & ocaml	letouzey
2001-04-24	cofix_warning dans les parametres d'extraction	filliatr
2001-04-24	Removing a debug message for the search command.	bertot
2001-04-23	forme code	filliatr
2001-04-23	mise a jour	letouzey
2001-04-23	realisation des reals	letouzey
2001-04-23	Gros nain avec de Bruijn...	letouzey
2001-04-23	divers	filliatr
2001-04-23	nettoyage	filliatr
2001-04-23	expansion des constr purs	filliatr
2001-04-23	Uncurryfy_ast inutile depuis l'eta-expansion dans extraction.ml.	letouzey
2001-04-23	Remaniement Makefile de test. make reals possible	letouzey
2001-04-20	Ajout Fourier	mayero
2001-04-20	optimizations extraction	filliatr
2001-04-20	Ajout des entetes	delahaye
2001-04-20	nettoyage	filliatr
2001-04-19	Add a treatement of elaborate Intros tactics, CONJPATTERN and family.	bertot
2001-04-19	scripts; extraction False_rec	filliatr
2001-04-19	blindage False_rec	filliatr
2001-04-19	cofix; axiomes; eta-expansions pour variables de types mal generalisees (en c...	filliatr
2001-04-19	ZArith --> Zarith	mohring
2001-04-19	synchonization des tables d'extraction	filliatr
2001-04-19	remplace Zarith par ZArith	mohring
2001-04-19	modifs des scripts de test auto	filliatr
2001-04-19	deplacement de l'optimisation inductif singleton	letouzey
2001-04-19	script de bench automatique pour extraction	letouzey
2001-04-19	Making sure there will be no warnings at compile time.	bertot
2001-04-19	Ajout de Field	delahaye
2001-04-18	Correcting a problem of s that appears behind a Let when there are	bertot
2001-04-18	Changing the commands to switch to textual explanation of proofs.	bertot
2001-04-18	Adding files for the production of textual explanations as used in pcoq.	bertot
2001-04-13	eliminiation des singletons du genre sig + divers	letouzey
2001-04-12	nouvelle gestion des variables de type ML	letouzey
2001-04-11	documentation automatique de la bibliothèque standard	filliatr
2001-04-11	réparation d'un bug de Correctness: whd_programs ne doit pas réduire les te...	filliatr
2001-04-10	bug dans eta-expansion des constructeurs. Argument Prop dans extract_type_app	letouzey
2001-04-10	portage exemples Correctness; changement du nom de pred_of_minus dans coq_omega	filliatr
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-09	exemples Correctness	filliatr
2001-04-09	branchement extraction en standard (pas de Require)	filliatr
2001-04-09	réparation Quote	filliatr
2001-04-08	Ajout lemmes arithmetiques	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-05	mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4	filliatr
2001-04-04	axiomes dans les types	filliatr
2001-04-04	renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...	filliatr
2001-04-04	implification de extract_constr et extract_term	letouzey