coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Revision of the FSetWeak Interface, so that it becomes a precise	letouzey	2007-10-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	subtype of the FSet Interface (and idem for FMapWeak / FMap). 1) No eq_dec is officially required in FSetWeakInterface.S.E (EqualityType instead of DecidableType). But of course, implementations still needs this eq_dec. 2) elements_3 differs in FSet and FSetWeak (sort vs. nodup). In FSetWeak we rename it into elements_3w, whereas in FSet we artificially add elements_3w along to the original elements_3. Initial steps toward factorization of FSetFacts and FSetWeakFacts, and so on... Even if it's not required, FSetWeakList provides a eq_dec on sets, allowing weak sets of weak sets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	As suggested by Pierre Casteran, fold for FSets/FMaps now takes a	letouzey	2007-05-27
\| \| \| \| \| \| \| \|	(A:Type) instead of a (A:Set). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Argument Scope de list déplacé dans List.v	herbelin	2006-07-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 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
*	+ ameliorating the tactic "functional induction"	jforest	2006-06-06
\| \| \| \| \| \| \| \|	+ bug correction in proof of structural principles + up do to date test-suite/success/Funind.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8899 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Replacing the old version of "functional induction" with the new one.	jforest	2006-05-31
\| \| \| \| \| \| \|	The old version is, for now, still available by prefixing any command/tactic with Old/old (eg. old functional induction ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8881 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* suite de la revision des wrappers Make	letouzey	2006-05-30
\| \| \| \| \| \| \|	* quelques unfold E.eq en cas de changement de la semantique des foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8876 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
*	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
*	reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵	letouzey	2006-03-28
\| \| \| \| \| \|	OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 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
*	Réparation de FSet (back to 8628)	notin	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8631 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation des $	letouzey	2006-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8629 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