coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Mise à jour scopes prédéfinis et Tactic Notation pour tacticals	herbelin	2006-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9012 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation 'external'	herbelin	2006-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correcting for bug #1167	jforest	2006-07-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9010 85f007b7-540e-0410-9357-904b9bb8a0f7
*	functional inversion now takes a quatified hypothesis as first argument	jforest	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9009 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ↵	herbelin	2006-07-04
\| \| \| \| \| \|	pattern pose problème pour les notations ajoutées à ce niveau; qu'à cela ne tienne, l'associativité du niveau 100 pour pattern n'est pas importante : on le rend RIGHTA git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9008 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Doc Print Grammar pattern	herbelin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9007 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation or-pattern	herbelin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9006 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation or-pattern	herbelin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9005 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout cible refman-quick qui teste la compilation sans faire les index, toc ↵	herbelin	2006-07-04
\| \| \| \| \| \|	et biblio git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adding comments and cleaning code	jforest	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9003 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo dans le manuel de référence	notin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9002 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' ↵	herbelin	2006-07-04
\| \| \| \| \| \|	+ modifs diverses de la présentation des règles d'inférence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9001 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- completely new version of "functional inversion" using inversion on	jforest	2006-07-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	inductive - bug correction in "Functional scheme" and "functional inversion": the function are now parsed as references and not indent - adding a zeta normalization function in rawtermops to zeta normalize graph constructions (not used for now) - Bug correction in generation of functional principle types (if an arguments of the function has a type which is a sort) - adding a new persistent table for functional induction informations (graph,...) - new save mechanism for functional induction principles (reuse of proofs when possible) - Minor bug correction in proof of principle. - Distinguishing building_principles (that is save them) and making then (just construct their proof term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ du manuel de référence	notin	2006-07-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test des motifs disjonctifs multiples	herbelin	2006-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8998 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin	2006-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise à jour (avec retard) des niveaux de la table default_pattern_levels	herbelin	2006-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8996 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ manuel de référence	notin	2006-07-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8995 85f007b7-540e-0410-9357-904b9bb8a0f7
*	forgot a file	jforest	2006-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8994 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug correction	jforest	2006-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8993 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte ↵	herbelin	2006-06-27
\| \| \| \| \| \|	des inductifs maintenant retourne des sortes d'inductives qui ne sont pas des variables) et test de non-régression git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8992 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans ↵	herbelin	2006-06-27
\| \| \| \| \| \|	l'environnement de preuve au moment de l'interprétation des arguments de tactiques (version 8971) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8991 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de Zgcd_spec (compat.)	notin	2006-06-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey	2006-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7
*	repetition d'hypotheses dans well_founded_induction_type_2	letouzey	2006-06-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8988 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stricte positivité en présence de types inductifs imbriqués avec ↵	herbelin	2006-06-23
\| \| \| \| \| \|	paramètres récursivement non uniformes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8987 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modifs de test-suite suite au passage des graphes de Function dans Type	jforest	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8986 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage des graphes de Function dans Type	jforest	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix wrong order of existentials in eterm.	msozeau	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8984 85f007b7-540e-0410-9357-904b9bb8a0f7
*	documentation	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8983 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT ↵	herbelin	2006-06-23
\| \| \| \| \| \|	EXTEND et TACTIC EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8982 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite passage ident -> hyp dans syntaxe de 'replace with in'	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8981 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouveau paragraphe sur le polymorphisme de sorte des inductifs	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8980 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suite utilisation hyp au lieu ident: donne la localisationn	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8979 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mention de coqide, proof general et pcoq	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction ident -> hyp pour dinterprÃ©ter des identificateurs devant ↵	herbelin	2006-06-23
\| \| \| \| \| \|	Ãªtre interprÃ©tÃ©s comme termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8977 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppresion redondance interp_entry_name entre Q_util et Argextend	herbelin	2006-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8976 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Préservation compatibilité interprétation quantified hypothesis ↵	herbelin	2006-06-23
\| \| \| \| \| \|	(provisoire ?) + export nouvelle macro pour maple.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deux vérifications que le polymorphisme de sorte des inductifs ne ↵	herbelin	2006-06-22
\| \| \| \| \| \|	fonctionne pas incorrectement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Légère mise à jour	herbelin	2006-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8973 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug du polymorphisme de sort des inductifs (cas où les variables ↵	herbelin	2006-06-22
\| \| \| \| \| \|	d'univers associées aux arités des paramètres ne sont pas distinctes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8972 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage, uniformisation	herbelin	2006-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8971 85f007b7-540e-0410-9357-904b9bb8a0f7
*	updated documentation for my tactics (P. orbineau	corbinea	2006-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8970 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added {measure x f} as a valid recursion order.	msozeau	2006-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mutually structurally recursive defs and rec using measures added.	msozeau	2006-06-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8968 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Harmonisation de l'interprétation des intropattern	herbelin	2006-06-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8967 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Wellfounded recursion using subtac working again.	msozeau	2006-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8966 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Progress in new wf def typing.	msozeau	2006-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8965 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rewrite of the recursive defs handling in progress.	msozeau	2006-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug serieux efficacite de ltac	barras	2006-06-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8963 85f007b7-540e-0410-9357-904b9bb8a0f7