Fix test-suite files, change conflicting notation "->rel" and the others

to "-R>" and the like. Split more precisely in inference of case
predicate between the new code which currently works only for matched
variables and the old one which works better on variables appearing in matched
terms types (the two could also be merged).


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

1 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v
index 72c7cc155..545b8aeb8 100644
--- a/test-suite/success/LetPat.v
+++ b/test-suite/success/LetPat.v
@@ -48,8 +48,8 @@ Definition identity_functor (c : category) : functor c c :=
     fun x => x.
 
 Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := 
-  let ' (A :& homA :& CA) := a in
-  let ' (B :& homB :& CB) := b in
-  let ' (C :& homB :& CB) := c in
+  let 'A :& homA :& CA := a in
+  let 'B :& homB :& CB := b in
+  let 'C :& homB :& CB := c in
     fun f g => 
-      fun x : A => g (f x).
+      fun x => g (f x).