coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Option --coqlib_path pour coqdoc (suite et fin)	notin	2006-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des warning gtk comme warning coq	herbelin	2006-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8776 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵	notin	2006-05-02
\| \| \| \| \| \|	Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug assert as	herbelin	2006-05-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite de l'ajout des FSets/FMaps dans les theories standards	letouzey	2006-04-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	-> OrderedTypeEx: des exemples de OrderedType -> OrderedTypeAlt: une definition alternative de OrderedType -> FSetAVL et FMapAVL: realisation a coup d'AVL -> FMapPositive: realisation a coup d'arbre binaire (selon les chiffres binaires de la cle) -> FMapIntMap : realisation en utilisant IntMap -> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine: on peut ne pas les compiler en passant l'option "-fsets no" a configure, de facon similaire a "-reals no" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleur nommage pour PairOrderedType	letouzey	2006-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8772 85f007b7-540e-0410-9357-904b9bb8a0f7
*	qq proprietes de plus sur Ncompare	letouzey	2006-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Continue l'écriture de la doc de "Function". Pas fini, manque:	courtieu	2006-04-28
\| \| \| \| \| \| \| \|	- relecture par YB et JF - adaptation de la partie functional induction - écriture de la partie functional inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8770 85f007b7-540e-0410-9357-904b9bb8a0f7
*	If function creates proof obligation, there are now printed once.	courtieu	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	r8931@thot: notin \| 2006-04-28 16:19:38 +0200	notin	2006-04-28
\| \| \| \| \| \| \| \|	Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8767 ↵	notin	2006-04-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8766 ↵	notin	2006-04-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8765 ↵	notin	2006-04-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8764 ↵	notin	2006-04-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8763 ↵	notin	2006-04-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8762 ↵	notin	2006-04-28
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout bug #1102	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵	notin	2006-04-28
\| \| \| \| \| \|	'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo dans précédent commit (8755); protection renforcée dans analyse ↵	herbelin	2006-04-28
\| \| \| \| \| \|	clause in du cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Distinction explicite des parties paramètres et arguments dans le type	herbelin	2006-04-27
\| \| \| \| \| \| \| \|	des inductifs de la clause "in" du filtrage. - Débogage et extension du parseur xml (g_xml.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Message d'erreur plus informatif	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Official MoWGLI definition of CIC dtd	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8753 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification of emacs output: No more show script at the end of a proof.	courtieu	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'entrée devdoc dans le Makefile principal et modification ↵	notin	2006-04-27
\| \| \| \| \| \|	en conséquence du Makefile dans dev/doc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la doc de l'option -stdout de coqdoc	notin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification of emacs output: Pp.warning and al now output warning	courtieu	2006-04-27
\| \| \| \| \| \| \| \| \| \| \|	between special characters. I had to add a hidden variable print_emacs and a function to set it to true in Pp because using Options.print_emacs would have introduce a circularity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8748 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification of emacs output: Pp.warning and al now output warning	courtieu	2006-04-27
\| \| \| \| \| \| \| \| \| \| \|	between special characters. I had to add a hidden variable print_emacs and a function to set it to true in Pp because using Options.print_emacs would have introduce a circularity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8747 85f007b7-540e-0410-9357-904b9bb8a0f7
*	préparation de add_glob en vue d'isolement de la partie module pour	herbelin	2006-04-27
\| \| \| \| \| \| \|	l'option glob-dump git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout chop_dirpath	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2-3 lemmes en plus pour que les Bvectors soient effectivement utilisables	letouzey	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8744 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a short doc for "Function". To be finished.	courtieu	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8743 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2006-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8742 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Utilisation d'abbréviations pour les types intervenant dans RCases	herbelin	2006-04-26
\| \| \| \| \| \| \| \| \|	- Factorisation du procédé de transformation Cases -> RCases dans Detyping - Rebranchement de la traduction XML pour Cases (interrompue depuis suppression traducteur) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8741 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Outil de test de la réversibilité du réafficheur v8->v8	herbelin	2006-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8740 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Diverses corrections de l'afficheur et du traducteur pour s'assurer de	herbelin	2006-04-26
\| \| \| \| \| \| \| \| \| \|	la réversibilité de la traduction (correction enregistrement des retours chariot dans le lexeur, correction affichage espace superflu en tête des VERNAC EXTEND, correction affichage morphism_signature dans extraargs.ml4, correction affichage clear dans pptactic.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Régénération après mise à jour coqdep pour traiter Require multiple	herbelin	2006-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8738 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte du Require multiple	herbelin	2006-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite du pont entre Bvector et N	letouzey	2006-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8736 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest	2006-04-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la ↵	notin	2006-04-26
\| \| \| \| \| \|	création du fichier de style git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8734 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Un gros coup de lifting pour IntMap:	letouzey	2006-04-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* le type ad des adresses est maintenant un alias vers le N de NArith, qui lui est isomorphe. * toutes les operations sur ces adresses (p.ex. un xor bit a bit) sont maintenant dans de nouveaux fichiers du repertoire NArith. * Intmap utilise maintenant le meme type option que le reste du monde * etc etc... Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs utilisant Intmap sont adaptees en consequence. Me demander si besoin ma moulinette d'adaptation (incomplete). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un lemme de double inclusion	letouzey	2006-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reverting nf_betaiotaevar_preserving_vm_cast	jforest	2006-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8731 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Code mort (suite)	herbelin	2006-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8730 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression code mort	herbelin	2006-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8729 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin	2006-04-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement anomaly en failwith dans out_name pour utilisation par map_succeed	herbelin	2006-04-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8727 85f007b7-540e-0410-9357-904b9bb8a0f7