summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-10-24 16:15:53 +0200
committerSon Ho2023-10-24 16:15:53 +0200
commitce4de37c76d85ed7795f4938cf212abd31668007 (patch)
tree413e89af22860b14fa799756c691b351dbe8f9cd
parentb2cbbb48494e8079eb000293e7734850e4ce3d05 (diff)
Fix an issue coming from the modification for the opaque signatures
-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 (