coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	+ 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
*	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
*	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
*	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
*	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