From 0b6924f05ef6beb775345f3fb2ad21a009ab3baa Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 29 Mar 2008 11:20:45 +0000
Subject: 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
---
 test-suite/bugs/closed/shouldsucceed/1784.v | 20 ++++++++++----------
 test-suite/success/LetPat.v                 |  8 ++++----
 2 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'test-suite')

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).
-- 
cgit v1.2.3