diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 647aa67492034e374d1ab239ac311fa8e3f714be..804de44d6069fac4856dafa2752858b2d8ebc0ff 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -16,13 +16,13 @@ Fixpoint is_list (hd : val) (xs : list val) : iProp :=
 
 Definition rev : val :=
   rec: "rev" "hd" "acc" :=
-    match: "hd" with
-      NONE => "acc"
+    match: '"hd" with
+      NONE => '"acc"
     | SOME "l" =>
-       let: "tmp1" := Fst !"l" in
-       let: "tmp2" := Snd !"l" in
-       "l" <- ("tmp1", "acc");;
-       "rev" "tmp2" "hd"
+       let: "tmp1" := Fst !'"l" in
+       let: "tmp2" := Snd !'"l" in
+       '"l" <- ('"tmp1", '"acc");;
+       '"rev" '"tmp2" '"hd"
     end.
 Global Opaque rev.