coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Doc Print Grammar pattern	herbelin	2006-07-04
*	Documentation or-pattern	herbelin	2006-07-04
*	Documentation or-pattern	herbelin	2006-07-04
*	Ajout cible refman-quick qui teste la compilation sans faire les index, toc e...	herbelin	2006-07-04
*	adding comments and cleaning code	jforest	2006-07-04
*	Typo dans le manuel de référence	notin	2006-07-04
*	Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' +...	herbelin	2006-07-04
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
*	MAJ du manuel de référence	notin	2006-07-04
*	Test des motifs disjonctifs multiples	herbelin	2006-07-03
*	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin	2006-07-03
*	Mise à jour (avec retard) des niveaux de la table default_pattern_levels	herbelin	2006-07-03
*	MAJ manuel de référence	notin	2006-07-03
*	forgot a file	jforest	2006-06-29
*	bug correction	jforest	2006-06-29
*	Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte de...	herbelin	2006-06-27
*	Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'...	herbelin	2006-06-27
*	Ajout de Zgcd_spec (compat.)	notin	2006-06-26
*	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey	2006-06-25
*	repetition d'hypotheses dans well_founded_induction_type_2	letouzey	2006-06-25
*	Stricte positivité en présence de types inductifs imbriqués avec paramètr...	herbelin	2006-06-23
*	modifs de test-suite suite au passage des graphes de Function dans Type	jforest	2006-06-23
*	Passage des graphes de Function dans Type	jforest	2006-06-23
*	Fix wrong order of existentials in eterm.	msozeau	2006-06-23
*	documentation	herbelin	2006-06-23
*	Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT E...	herbelin	2006-06-23
*	Suite passage ident -> hyp dans syntaxe de 'replace with in'	herbelin	2006-06-23
*	Nouveau paragraphe sur le polymorphisme de sorte des inductifs	herbelin	2006-06-23
*	Suite utilisation hyp au lieu ident: donne la localisationn	herbelin	2006-06-23
*	Mention de coqide, proof general et pcoq	herbelin	2006-06-23
*	Correction ident -> hyp pour dinterprÃ©ter des identificateurs devant Ãªt...	herbelin	2006-06-23
*	Suppresion redondance interp_entry_name entre Q_util et Argextend	herbelin	2006-06-23
*	Préservation compatibilité interprétation quantified hypothesis (provisoir...	herbelin	2006-06-23
*	Deux vérifications que le polymorphisme de sorte des inductifs ne fonctionne...	herbelin	2006-06-22
*	Légère mise à jour	herbelin	2006-06-22
*	Correction bug du polymorphisme de sort des inductifs (cas où les variables ...	herbelin	2006-06-22
*	Nettoyage, uniformisation	herbelin	2006-06-22
*	updated documentation for my tactics (P. orbineau	corbinea	2006-06-22
*	Added {measure x f} as a valid recursion order.	msozeau	2006-06-22
*	Mutually structurally recursive defs and rec using measures added.	msozeau	2006-06-22
*	Harmonisation de l'interprétation des intropattern	herbelin	2006-06-21
*	Wellfounded recursion using subtac working again.	msozeau	2006-06-20
*	Progress in new wf def typing.	msozeau	2006-06-20
*	Rewrite of the recursive defs handling in progress.	msozeau	2006-06-20
*	bug serieux efficacite de ltac	barras	2006-06-19
*	Ajout de tactiques expérimentales basée sur functional induction.	courtieu	2006-06-16
*	Report des modifications faites lors de la 8.0pl3 (ter)	notin	2006-06-15
*	Report des modifications faites lors de la 8.0pl3 (bis)	notin	2006-06-15
*	Report des modifications faites lors de la 8.0pl3	notin	2006-06-15
*	Typo in case of reference to dev/doc/changes.txt	lmamane	2006-06-15