coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Quick hack to solve to complexity issue in function mark_occur	herbelin	2006-11-01
*	Ajout test setoid_rewrite (cf bug #1176); anglicisation	herbelin	2006-11-01
*	Debug obligation handling code	msozeau	2006-10-31
*	Retour sur la modification apportée en r9289, et nouvelle correction du bug ...	notin	2006-10-31
*	Fix compile error	msozeau	2006-10-31
*	Work on obligation separation.	msozeau	2006-10-31
*	syntaxe du let in encore	barras	2006-10-31
*	assouplissement de la syntaxe du let de ltac: t1 ; let in autorise	barras	2006-10-31
*	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin	2006-10-30
*	MAJ	herbelin	2006-10-30
*	typo	herbelin	2006-10-30
*	dependences	barras	2006-10-30
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30
*	missing Require LegacyRfield	barras	2006-10-30
*	LegacyRfield was opening R_scope	barras	2006-10-30
*	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-29
*	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-28
*	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-27
*	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-26
*	Applatissement des noeuds application vide dans le filtrage Ltac (ex:	herbelin	2006-10-25