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

5 files changed, 38 insertions, 34 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e1c5beeea2..7c0ed946f5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1586,28 +1586,28 @@ let prepare_predicate_from_arsign_tycon loc env evdref tomatchs sign arsign c =
  * tycon to make the predicate if it is not closed.
  *)
 
+let is_dependent_on_rel x t =
+  match kind_of_term x with
+      Rel n -> not (noccur_with_meta n n t)
+    | _ -> false
+
 let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function
   (* No type annotation *)
   | None ->
       (match tycon with
        | Some (None, t) ->
-	   if noccur_with_meta 0 max_int t then
-	     let names,pred =
-	       prepare_predicate_from_tycon loc false env evdref tomatchs sign t
-	     in
-	       Some (build_initial_predicate false names pred)
-	   else
+	   if List.exists (fun (x,_) -> is_dependent_on_rel x t) tomatchs
+	   then
 	     let arsign = extract_arity_signature env tomatchs sign in
 	     let env' = List.fold_right push_rels arsign env in
 	     let names = List.rev (List.map (List.map pi1) arsign) in
 	     let pred = prepare_predicate_from_arsign_tycon loc env' evdref tomatchs sign arsign t in
-	       if eq_constr pred t then
-		 let names,pred =
-		   prepare_predicate_from_tycon loc false env evdref tomatchs sign t
-		 in
-		   Some (build_initial_predicate false names pred)
-	       else
-		 Some (build_initial_predicate true names pred)
+	       Some (build_initial_predicate true names pred)
+	   else
+	     let names,pred =
+	       prepare_predicate_from_tycon loc false env evdref tomatchs sign t
+	     in
+	       Some (build_initial_predicate false names pred)
        | _ -> None)
 
   (* Some type annotation *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 6778831d85..12c92a8f7f 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,30 +58,30 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
   match x with
     | I x => 
       match y with
-        | I y => if (Z_eq_dec x y) then left else right
-        | S ys => right
+        | I y => if (Z_eq_dec x y) then in_left else in_right
+        | S ys => in_right
       end
     | S xs => 
       match y with
-        | I y => right
+        | I y => in_right
         | S ys =>
           let fix list_in (xs ys:list sv) {struct xs} : 
             {slist_in xs ys} + {~slist_in xs ys} :=
             match xs with
-              | nil => left
+              | nil => in_left
               | x::xs =>
                 let fix elem_in (ys:list sv) : {sin x ys}+{~sin x ys} :=
                   match ys with
-                    | nil => right
-                    | y::ys => if lt_dec x y then left else if elem_in
-                      ys then left else right
+                    | nil => in_right
+                    | y::ys => if lt_dec x y then in_left else if elem_in
+                      ys then in_left else in_right
                   end
                 in 
                 if elem_in ys then 
-                  if list_in xs ys then left else right
-                else right
+                  if list_in xs ys then in_left else in_right
+                else in_right
             end
-            in if list_in xs ys then left else right
+            in if list_in xs ys then in_left else in_right
       end
   end.
 
diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v
index 72c7cc1553..545b8aeb86 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).
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 4765bf0eea..c7e199b62b 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -20,6 +20,8 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
+Open Local Scope relation_scope.
+
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -445,7 +447,7 @@ Proof.
 Qed.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
-  inverse (R ==> R') <->rel (inverse R ==> inverse R').
+  inverse (R ==> R') <R> (inverse R ==> inverse R').
 Proof.
   intros.
   unfold flip, respectful.
@@ -591,5 +593,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism :
   Qed.
 
 Lemma inverse_pointwise_relation A (R : relation A) : 
-  pointwise_relation (inverse R) <->rel inverse (pointwise_relation (A:=A) R).
+  pointwise_relation (inverse R) <R> inverse (pointwise_relation (A:=A) R).
 Proof. reflexivity. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 3d5c6a7ee4..cb32b846d7 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -219,24 +219,26 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
 Definition relation_equivalence {A : Type} : relation (relation A) :=
   fun (R R' : relation A) => forall x y, R x y <-> R' x y.
 
-Infix "<->rel" := relation_equivalence (at level 70).
+Infix "<R>" := relation_equivalence (at level 70) : relation_scope.
 
 Class subrelation {A:Type} (R R' : relation A) :=
   is_subrelation : forall x y, R x y -> R' x y.
 
 Implicit Arguments subrelation [[A]].
 
-Infix "->rel" := subrelation (at level 70).
+Infix "-R>" := subrelation (at level 70) : relation_scope.
 
 Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
   fun x y => R x y /\ R' x y.
 
-Infix "//\\" := relation_conjunction (at level 55).
+Infix "/R\" := relation_conjunction (at level 55) : relation_scope.
 
 Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
   fun x y => R x y \/ R' x y.
 
-Infix "\\//" := relation_disjunction (at level 55).
+Infix "\R/" := relation_disjunction (at level 55) : relation_scope.
+
+Open Local Scope relation_scope.
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
@@ -258,7 +260,7 @@ Program Instance subrelation_preorder :
    on the carrier. *)
 
 Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
-  partial_order_equivalence : relation_equivalence eqA (R //\\ flip R).
+  partial_order_equivalence : relation_equivalence eqA (R /R\ flip R).
 
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism