From 47691de8fe3dc32a29663d4d8343eb415ce1d81e Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Thu, 30 Jun 2022 12:22:14 +0200
Subject: Traduct globals body separately (WIP)

---
 fstar/Primitives.fst | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'fstar')

diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst
index fe351f3a..b3da25c2 100644
--- a/fstar/Primitives.fst
+++ b/fstar/Primitives.fst
@@ -34,6 +34,9 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
+// Unwrap a successful result by normalisation (used for globals).
+let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
+
 (*** Misc *)
 type char = FStar.Char.char
 type string = string
-- 
cgit v1.2.3


From 6b6bbb9fcd56501b4f6ab1c6c16b9878a49aaadd Mon Sep 17 00:00:00 2001
From: Son HO
Date: Thu, 22 Sep 2022 16:35:29 +0200
Subject: Update fstar/Primitives.fst

---
 fstar/Primitives.fst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'fstar')

diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst
index b3da25c2..b44fe9d1 100644
--- a/fstar/Primitives.fst
+++ b/fstar/Primitives.fst
@@ -34,7 +34,7 @@ let bind (#a #b : Type0) (m : result a) (f : a -> result b) : result b =
 // Monadic assert(...)
 let massert (b:bool) : result unit = if b then Return () else Fail
 
-// Unwrap a successful result by normalisation (used for globals).
+// Normalize and unwrap a successful result (used for globals).
 let eval_global (#a : Type0) (x : result a{Return? (normalize_term x)}) : a = Return?.v x
 
 (*** Misc *)
-- 
cgit v1.2.3