coq/test-suite/success/setoid_test_function_space.v8, branch master The formal proof system Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8 2005-12-21T23:50:17+00:00 herbelin 2005-12-21T23:50:17+00:00 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7 
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
A wish by Bas Spitters granted: a little more of unification up to 2005-05-19T13:03:45+00:00 sacerdot 2005-05-19T13:03:45+00:00 d55637238606e1f3eba48219266782d691e021ad convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7 
convertibility is now tried in setoid_rewrite. As a consequence it is now
possible to declare relations over the function space (fun A B: Type => A -> B).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7