summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ExtractToFStar.ml12
1 files changed, 10 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 6fd141cc..26316bc4 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -203,7 +203,15 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
* type t = { x : int; y : bool; }
* ```
*
- * Or if there isn't enough space on one line:
+ * If there isn't enough space on one line:
+ * ```
+ * type t =
+ * {
+ * x : int; y : bool;
+ * }
+ * ```
+ *
+ * And if there is even less space:
* ```
* type t =
* {
@@ -211,11 +219,11 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
* y : bool;
* }
* ```
- * Note that we already printed: `type t =`
*
* Also, in case there are no fields, we need to define the type as `unit`
* (`type t = {}` doesn't work in F* ).
*)
+ (* Note that we already printed: `type t =` *)
if fields = [] then (
F.pp_print_space fmt ();
F.pp_print_string fmt "unit")