coq - The formal proof system

Age	Commit message (Expand)	Author
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-03	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-06-29	forgot a file	jforest
2006-06-29	bug correction	jforest
2006-06-27	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-26	Ajout de Zgcd_spec (compat.)	notin
2006-06-25	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey
2006-06-25	repetition d'hypotheses dans well_founded_induction_type_2	letouzey
2006-06-23	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-22	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-21	Harmonisation de l'interprétation des intropattern	herbelin
2006-06-20	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-19	bug serieux efficacite de ltac	barras
2006-06-16	Ajout de tactiques expérimentales basée sur functional induction.	courtieu
2006-06-15	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	MAJ	herbelin
2006-06-14	MAJ	herbelin
2006-06-14	A list of incompatibilities	herbelin
2006-06-13	ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...	jforest