typing/tests: make all the functions values as they should be

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

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

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

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