summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon HO2022-09-22 16:27:29 +0200
committerGitHub2022-09-22 16:27:29 +0200
commit5080fa9c40fb8adfd87bd957cd1beca6c7e8e98e (patch)
tree33403b48029862d0832b9055764ffd558859188f
parent08e46b0dae3532ed646e6d39894726700d066a50 (diff)
Update src/ExtractToFStar.ml
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 5e33566f..f2ea9945 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -1549,7 +1549,7 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
For example in Rust,
`static X: u32 = 3;`
- will be translated to
+ will be translated to:
`let x_body : result int = Return 3`
`let x_c : int = eval_global x_body`
*)