From bb0a959a60002dd59bc0e81104a7234c4e008c03 Mon Sep 17 00:00:00 2001 From: Maxime Buyse Date: Mon, 23 Dec 2024 16:08:11 +0100 Subject: [PATCH] Filter Impl after adding comments. --- engine/backends/fstar/fstar_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 4dc350d1f..1c900ef19 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -1608,7 +1608,6 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) : [%matches? (Types.Included None' : Types.inclusion_kind)] interface_mode' in Print.pitem item - |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true) |> List.concat_map ~f:(function | `Impl i -> [ (mk_impl (Print.decl_to_string i), `Newline) ] | `Intf i -> [ (mk_intf (Print.decl_to_string i), `Newline) ] @@ -1618,6 +1617,7 @@ let strings_of_item (bo : BackendOptions.t) m items (item : item) : let s = "(* " ^ s ^ " *)" in if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ] else [ (`Impl s, `Newline) ]) + |> List.filter ~f:(function `Impl _, _ when no_impl -> false | _ -> true) type rec_prefix = NonRec | FirstMutRec | MutRec