coq - The formal proof system

Age	Commit message (Expand)	Author
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
2006-06-13	Changement du index.html généré dans refman	notin
2006-06-13	rearrangement du code: deplacement du code effectuant functional	courtieu
2006-06-12	Typo in replace doc.	jforest
2006-06-12	Updating documentation of replace and correcting a typo in error message of r...	jforest
2006-06-12	changed comments.	courtieu
2006-06-12	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 85f007b7-540e-04...	jforest
2006-06-10	Bug is_number	herbelin
2006-06-10	MAJ fichier dev/doc/changes.txt	herbelin
2006-06-10	ajout de la doc sur l'option -enable-geoproof de CoqIDE	jnarboux
2006-06-09	Suppression du répertoire distrib: il fait désormais partie du projet coq-d...	notin
2006-06-09	Commit doc Claudio Sacerdoti	herbelin
2006-06-09	Nouvelle MAJ	herbelin
2006-06-09	Déplacement vers archive coq-dev-tools/distrib	herbelin
2006-06-09	Nouvelle MAJ	herbelin
2006-06-09	ajout de la doc de classical_right et left	jnarboux
2006-06-09	MAJ liste fichiers doc stdlib	herbelin
2006-06-09	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin
2006-06-09	Adaptation Tactics.out et Cases.out au comportement actuel à défaut d'évit...	herbelin
2006-06-09	Bug suite déplacement Int.v dans ZArith	herbelin
2006-06-09	Déplacement Int.v dans ZArith, déplacement de DecidableType.v et DecidableT...	herbelin
2006-06-09	Ajout d'une option -with-geoproof à la configuration et à l'exécution	notin
2006-06-09	oups: il faut penser a fermer la porte en partant (d'un fixpoint)	letouzey
2006-06-09	changements de dernieres minutes pour la 8.1 beta:	letouzey
2006-06-08	Plus de Declare Module sans vrai type explicite	herbelin