diff options
Diffstat (limited to 'compiler/ExtractBuiltin.ml')
| -rw-r--r-- | compiler/ExtractBuiltin.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 2dbacce3..c6bde9c2 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -149,7 +149,10 @@ let builtin_types () : builtin_type_info list = let fields = List.map (fun (rname, name) -> - (rname, backend_choice (extract_name ^ name) name)) + ( rname, + match !backend with + | FStar | Lean -> name + | Coq | HOL4 -> extract_name ^ "_" ^ name )) fields in let constructor = mk_struct_constructor extract_name in |