1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 00a13aed..3b7f0d84 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -22,14 +22,14 @@ Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
 Print merge.
 
 
-Print Zlt.
+Print Z.lt.
 Print Zwf.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
   match n ?= m with
-    | Lt => Zwfrec n (Zpred m)
+    | Lt => Zwfrec n (Z.pred m)
     | _ => 0
   end.