2 files changed, 14 insertions, 14 deletions
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).