coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Typo in a comment	letouzey	2009-07-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12243 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Various little fixes:	msozeau	2009-01-18
\| \| \| \| \| \| \| \| \| \| \| \|	- allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
*	FMaps: various updates (mostly suggested by P. Casteran)	letouzey	2008-12-26
\| \| \| \| \| \| \| \| \| \| \| \| \|	- New functions: update (a kind of union), restrict (a kind of inter), diff. - New predicat Partition (and Disjoint), many results about Partition. - Equivalence instead of obsolete Setoid_Theory (they are aliases). refl_st, sym_st, trans_st aren't used anymore and marked as obsolete. - Start using Morphism (E.eq==>...) instead of compat_... This change (FMaps only) is incompatible with 8.2betaX, but it's really better now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11718 85f007b7-540e-0410-9357-904b9bb8a0f7
*	FMap: fold_rec + more permissive transpose hyp + various cleanup	letouzey	2008-12-22
\| \| \| \| \| \| \|	The induction principles for fold are due to S. Lescuyer The better transpose hyp is a suggestion by P. Casteran git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11711 85f007b7-540e-0410-9357-904b9bb8a0f7
*	migration from Set to Type of FSet/FMap + some dependencies...	letouzey	2008-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
\| \| \| \| \| \| \| \|	more general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Extensions of FMap(Weak)Facts:	letouzey	2007-06-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	fold properties and induction principles for (weak) maps. - Simplification in SetoidList: the two important results fold_right_equivlistA and fold_right_add are now proved without using removeA and hence do not depend anymore on a decidable equality (good for maps and their arbitrary datas). In fact, removeA is not used at all anymore, but I leave it here (mostly), since it can't hurt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9914 85f007b7-540e-0410-9357-904b9bb8a0f7
*	additional properties for FMap (and slight rework of SetoidList and ↵	letouzey	2007-06-26
\| \| \| \| \| \|	FSetProperties) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9908 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oups: one file forgotten in my previous commit	letouzey	2007-06-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9891 85f007b7-540e-0410-9357-904b9bb8a0f7
*	some more properties of fold and elements in FSetProperties	letouzey	2007-06-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9885 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de prÃ©cÃ©dence de l'argument du by de assert; ↵	herbelin	2006-05-23
\| \| \| \| \| \|	consÃ©quences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un debut de propriétés concernant FMap	letouzey	2006-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petit ajout concernant InA	letouzey	2006-05-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8818 85f007b7-540e-0410-9357-904b9bb8a0f7
*	decidabilite de InA	letouzey	2006-05-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8807 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Duplication du fichier FSetProperties pour les ensembles Weak.	letouzey	2006-05-11
\| \| \| \| \| \| \| \| \| \|	Du coup, factorisation d'une partie dans SetoidList. Ajout de lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface concernant elements. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7
*	versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes	letouzey	2006-04-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
*	propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble ↵	letouzey	2006-03-16
\| \| \| \| \| \|	des fichiers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	utilisation de removeA dans FSetProperties	letouzey	2006-03-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	renommage NoRedun vers le plus joli NoDup	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8635 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de fonctions sur les listes	notin	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8632 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de theories/FSets contenant la partie "light" de FSets et FMap:	letouzey	2006-03-15
	pas d'implementations par AVL, mais celles par lists, ainsi que les foncteurs de proprietes. Au passage, ajout de MoreList (complements de List) et SetoidList (quelques relations sur des listes considerees modulo un eq ou lt non standard. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8628 85f007b7-540e-0410-9357-904b9bb8a0f7