coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-30	missing Require LegacyRfield	barras
2006-10-30	LegacyRfield was opening R_scope	barras
2006-10-29	Suite commit polymorphisme	herbelin
2006-10-29	Exports manquants dans ring	barras
2006-10-29	Compatibilité du polymorphisme de constantes avec les sections.	herbelin
2006-10-28	MAJ nouvelles théories	herbelin
2006-10-28	Prise en compte dépendance de subtyping en typeops (polymorphisme de defs)	herbelin
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-10-28	MAJ	herbelin
2006-10-28	Suite commit 9256: autres cas incorrects de prise en compte de @ dans les ident	herbelin
2006-10-28	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin
2006-10-28	Fixes in experimental merging of functional graphs.	courtieu
2006-10-28	Ajout option Set Printing Universes et amélioration affichage des univers	herbelin
2006-10-27	Ajout fold_rel_declaration et fold_named_declaration	herbelin
2006-10-27	simplif de la partie ML de ring/field	barras
2006-10-27	Correction de 2 bugs critiques du polymorphisme d'univers	herbelin
2006-10-27	Fixes on functional graphs merging: put functional results at the end	courtieu
2006-10-27	changement des _sym par _comm dans setoid_ring	bgregoir
2006-10-27	Le caractère ² fait planter make doc	notin
2006-10-27	Check that sort-polymorphic inductive types is not too lax	herbelin
2006-10-27	Fixes on functional graphs merging: removed debug printing.	courtieu
2006-10-27	Fixes on functional graphs merging: names of constructors.	courtieu
2006-10-27	Cette dérivation de paradoxe passait en V8.1beta	herbelin
2006-10-27	Restriction au implémenteurs	herbelin
2006-10-27	Ajout ListTactics	herbelin
2006-10-27	Ajout ListTactics	herbelin
2006-10-26	Déplacement des propriétés générales de BinList dans List et des tactiqu...	herbelin
2006-10-26	Affichage d'un message d'erreur losque qu'une relation n'a pas été déclar�...	notin
2006-10-26	Noms de compatibilité déplacés en bloc à la fin du fichier	herbelin
2006-10-26	Some fixes in experimental merging of two functional graphs.	courtieu
2006-10-26	added doc for declarative language	corbinea
2006-10-26	Experimental merging of two functional graphs.	courtieu
2006-10-26	Facilities to automatically solve obligations	msozeau
2006-10-26	MAJ crédits, fresh; documentation apply in	herbelin
2006-10-26	MAJ	herbelin
2006-10-26	Petit bug apply in	herbelin
2006-10-25	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin
2006-10-25	Suite commit 9277	herbelin
2006-10-25	oups, ne chargeait pas les bons fichiers	letouzey
2006-10-25	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin
2006-10-25	coqdep -slash	barras
2006-10-25	Ménage	notin
2006-10-25	oops	barras
2006-10-25	conflit de nom (Field_theory) modulo la casse	barras
2006-10-24	Extension de fresh (suite)	herbelin
2006-10-24	Changement de la valeur par défaut de with_geoproof (stabilité coqide)	notin
2006-10-24	Test apply in	herbelin
2006-10-24	Insère une coercion vers Sortclass dans 'contradiction' si nécessaire	herbelin
2006-10-24	Ajout de la tactique 'remember'	herbelin
2006-10-24	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin