diff options
Diffstat (limited to 'compiler/Translate.ml')
| -rw-r--r-- | compiler/Translate.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 347052a8..781766ee 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -796,7 +796,11 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Initialize the extraction context - for now we extract only to F*. * We initialize the names map by registering the keywords used in the * language, as well as some primitive names ("u32", etc.) *) - let variant_concatenate_type_name = true in + let variant_concatenate_type_name = + (* For Lean, we exploit the fact that the variant name should always be + prefixed with the type name to prevent collisions *) + match !Config.backend with Coq | FStar -> true | Lean -> false + in let mk_formatter_and_names_map = Extract.mk_formatter_and_names_map in let fmt, names_map = mk_formatter_and_names_map trans_ctx crate.name |