summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/ExtractTypes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 5446f912..15e75da2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -40,7 +40,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
F.pp_print_string fmt ("%" ^ iname)
| Lean ->
let iname = String.lowercase_ascii (int_name sv.int_ty) in
- F.pp_print_string fmt iname
+ F.pp_print_string fmt ("#" ^ iname)
| HOL4 -> ()
| _ -> craise __FILE__ __LINE__ span "Unreachable");
if print_brackets then F.pp_print_string fmt ")")