diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index cc8982e4b4d5f8f82a18052ed4d16ec74b6e91aa..4973fd2e39fffc9bc428c48bb7d048abb635fb11 100644
--- a/theories/typing/tests/get_x.v
+++ b/theories/typing/tests/get_x.v
@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
 Section get_x.
   Context `{typeG Σ}.
 
-  Definition get_x :=
-    (funrec: <> ["p"] :=
+  Definition get_x : val :=
+    funrec: <> ["p"] :=
        let: "p'" := !"p" in
        letalloc: "r" := "p'" +â‚— #0 in
-       delete [ #1; "p"] ;; "return" ["r":expr])%E.
+       delete [ #1; "p"] ;; "return" ["r":expr].
 
   Lemma get_x_type :
     typed_instruction_ty [] [] [] get_x
diff --git a/theories/typing/tests/init_prod.v b/theories/typing/tests/init_prod.v
index f8cd890a92b0e7f2cc6db738a1debba94d9ecbb9..827d339702e296f7e106272180e39aa2ae617548 100644
--- a/theories/typing/tests/init_prod.v
+++ b/theories/typing/tests/init_prod.v
@@ -7,12 +7,12 @@ Set Default Proof Using "Type".
 Section rebor.
   Context `{typeG Σ}.
 
-  Definition init_prod :=
-    (funrec: <> ["x"; "y"] :=
+  Definition init_prod : val :=
+    funrec: <> ["x"; "y"] :=
        let: "x'" := !"x" in let: "y'" := !"y" in
        let: "r" := new [ #2] in
        "r" +â‚— #0 <- "x'";; "r" +â‚— #1 <- "y'";;
-       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r":expr])%E.
+       delete [ #1; "x"] ;; delete [ #1; "y"] ;; "return" ["r":expr].
 
   Lemma init_prod_type :
     typed_instruction_ty [] [] [] init_prod
diff --git a/theories/typing/tests/rebor.v b/theories/typing/tests/rebor.v
index cae48c5a029b2629fb8080d6dcae0a7695320695..bdb8cd0a6b60df168df9faca3723581080d08cc8 100644
--- a/theories/typing/tests/rebor.v
+++ b/theories/typing/tests/rebor.v
@@ -7,8 +7,8 @@ Set Default Proof Using "Type".
 Section rebor.
   Context `{typeG Σ}.
 
-  Definition rebor :=
-    (funrec: <> ["t1"; "t2"] :=
+  Definition rebor : val :=
+    funrec: <> ["t1"; "t2"] :=
        Newlft;;
        letalloc: "x" := "t1" in
        let: "x'" := !"x" in let: "y" := "x'" +â‚— #0 in
@@ -16,7 +16,7 @@ Section rebor.
        let: "y'" := !"y" in
        letalloc: "r" := "y'" in
        Endlft ;; delete [ #2; "t1"] ;; delete [ #2; "t2"] ;;
-                 delete [ #1; "x"] ;; "return" ["r":expr])%E.
+                 delete [ #1; "x"] ;; "return" ["r":expr].
 
   Lemma rebor_type :
     typed_instruction_ty [] [] [] rebor
diff --git a/theories/typing/tests/unbox.v b/theories/typing/tests/unbox.v
index aca132b1ba7b570770cb0627f721681c5af8f10f..b807b8c390da60d28215f74afc2d58c2e9a9a4f2 100644
--- a/theories/typing/tests/unbox.v
+++ b/theories/typing/tests/unbox.v
@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
 Section unbox.
   Context `{typeG Σ}.
 
-  Definition unbox :=
-    (funrec: <> ["b"] :=
+  Definition unbox : val :=
+    funrec: <> ["b"] :=
        let: "b'" := !"b" in let: "bx" := !"b'" in
        letalloc: "r" := "bx" +â‚— #0 in
-       delete [ #1; "b"] ;; "return" ["r":expr])%E.
+       delete [ #1; "b"] ;; "return" ["r":expr].
 
   Lemma ubox_type :
     typed_instruction_ty [] [] [] unbox