summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-04-27 15:55:36 +0200
committerSon Ho2022-04-27 15:55:36 +0200
commit122dc6bfe7075fef7389c716ba2cc1aa7ed2fe02 (patch)
tree0881183f365a63e3f54afd15ae2ba5b176fe6012
parent018278ff418da62d1391c5f500def96890602f5a (diff)
Fix a minor issue
Diffstat (limited to '')
-rw-r--r--src/ExtractToFStar.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index f0ec73f5..e9b91c6e 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -986,7 +986,8 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
extract_typed_lvalue ctx fmt true x)
ctx xl
in
- F.pp_print_string fmt ".";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "->";
F.pp_print_space fmt ();
(* Print the body *)
extract_texpression ctx fmt false e;