summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml19
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 (