Fix an issue coming from the modification for the opaque signatures

1 files changed, 7 insertions, 12 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 0260b78b..b1c65be9 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -3674,18 +3674,13 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   let use_forall =
     is_opaque_coq && def.signature.generics <> empty_generic_params
   in
-  (* Print the qualifier ("assume", etc.).
-
-     if `wrap_opaque_in_sig`: we generate a record of assumed funcions.
-     TODO: this is obsolete.
-  *)
-  (if not (kind = Assumed || kind = Declared) then
-     let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
-     match qualif with
-     | Some qualif ->
-         F.pp_print_string fmt qualif;
-         F.pp_print_space fmt ()
-     | None -> ());
+  (* Print the qualifier ("assume", etc.). *)
+  let qualif = ctx.fmt.fun_decl_kind_to_qualif kind in
+  (match qualif with
+  | Some qualif ->
+      F.pp_print_string fmt qualif;
+      F.pp_print_space fmt ()
+  | None -> ());
   F.pp_print_string fmt def_name;
   F.pp_print_space fmt ();
   if use_forall then (