5 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 495a16bca2..ee9e2504a6 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -26,13 +26,13 @@ Program Fixpoint union
     | t1,Leaf => t1
     | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
         if (Z_ge_lt_dec h1 h2) then
-          if (Z_eq_dec h2 1)
+          if (Z.eq_dec h2 1)
           then add v2 s
           else
             let (l2', r2') := split v1 u in
             join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
         else
-          if (Z_eq_dec h1 1)
+          if (Z.eq_dec h1 1)
           then add v1 s
           else
             let (l1', r1') := split v2 u in
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 718b0e8611..fb2f0ca90e 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,7 +58,7 @@ 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 in_left else in_right
+        | I y => if (Z.eq_dec x y) then in_left else in_right
         | S ys => in_right
       end
     | S xs =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 5627612f6d..17eeb35291 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -1,6 +1,6 @@
 Require Import ZArith.
 
-Definition zeq := Z_eq_dec.
+Definition zeq := Z.eq_dec.
 
 Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
  fun y => if zeq x y then v else s y.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 72396d4903..d583761985 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -13,7 +13,7 @@ Qed.
 
 Require Import ZArith.
 
-Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt.
 
 Lemma f_refl'' : forall n , f'' true n n.
 Proof.
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 0fc854b6fd..142ada268b 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -1,8 +1,8 @@
-(* Check that "apply refl_equal" is not exported as an interactive
+(* Check that "apply eq_refl" is not exported as an interactive
    tactic but as a statically globalized one *)
 
 (* (this is a simplification of the original bug report) *)
 
 Module A.
-Hint Rewrite sym_equal using apply refl_equal : foo.
+Hint Rewrite eq_sym using apply eq_refl : foo.
 End A.