coq - The formal proof system

Age	Commit message (Expand)	Author
2006-11-13	Correction typo	herbelin
2006-11-11	Fichiers obsolètes	herbelin
2006-11-11	Typo + ajout Qcanon.v	herbelin
2006-11-10	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin
2006-11-10	generalisation de ring pour faire Ring_nf	barras
2006-11-10	Work on mutual defs, various bug fixes.	msozeau
2006-11-10	Correction d'un bug refine	herbelin
2006-11-10	Work on pattern inequalities for pattern matching branches.	msozeau
2006-11-09	Support for mutual defs in obligation handling.	msozeau
2006-11-07	Changement des modifeurs par défaut dans CoqIDE (problème de compatibilité...	notin
2006-11-07	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9348 85f007b7-540e-04...	filliatr
2006-11-06	Changement du magic number	notin
2006-11-05	fixes PR#1269 about function: there is no reason well founded induction is	bertot
2006-11-03	Suppression source de complexité polynomiale introduite par le polymorphisme	herbelin
2006-11-03	bug test complexité	herbelin
2006-11-02	gestion speciale du niveau 5 des ltac	barras
2006-11-02	Add doc on obligation solving commands.	msozeau
2006-11-01	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-10-31	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-30	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-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