summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-09-04 01:09:22 +0200
committerSon Ho2023-09-04 01:09:22 +0200
commite18160aa7a796989cc6ff7c953ee088023a3ea93 (patch)
tree8ff39fcae0efbe156ab589d89a65b01d9f5309dd /compiler
parent3151e373d64f9bce6146a44cd2d3cc64cac84cbf (diff)
Fix a minor issue in HOL4
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 8aee8c4f..de6c2fc8 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1239,7 +1239,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
| Assumed _ -> true
| _ -> raise (Failure "Unreachable")
in
- if const_generics <> [] && print_tys then (
+ if types <> [] && print_tys then (
let print_paren = List.length types > 1 in
if print_paren then F.pp_print_string fmt "(";
Collections.List.iter_link