summaryrefslogtreecommitdiff
path: root/tests/betree
diff options
context:
space:
mode:
authorSon Ho2022-09-22 17:27:24 +0200
committerSon Ho2022-09-22 17:27:24 +0200
commite18bf82b0931a7fd8a357a8516ef8618d77d42cf (patch)
tree51002290953b53ce4aa974babe23c588321311ef /tests/betree
parent798876feed0e06923f4066a8d04b87081fef72e0 (diff)
Regenerate the translated files
Diffstat (limited to 'tests/betree')
-rw-r--r--tests/betree/Primitives.fst2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index b3da25c2..b44fe9d1 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/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 *)