From 81c01a0e2d776e437fe12436f75b0338620061af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Jan 2017 15:20:48 +0100
Subject: [PATCH] typing/tests: make all the functions values as they should be

---
 theories/typing/tests/get_x.v     | 6 +++---
 theories/typing/tests/init_prod.v | 6 +++---
 theories/typing/tests/rebor.v     | 6 +++---
 theories/typing/tests/unbox.v     | 6 +++---
 4 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/theories/typing/tests/get_x.v b/theories/typing/tests/get_x.v
index cc8982e4..4973fd2e 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 f8cd890a..827d3397 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 cae48c5a..bdb8cd0a 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 aca132b1..b807b8c3 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
-- 
GitLab