diff options
Diffstat (limited to 'compiler/ExtractBase.ml')
-rw-r--r-- | compiler/ExtractBase.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index f8d3cd96..ce8c38ba 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1679,9 +1679,11 @@ let ctx_compute_var_basename (meta : Meta.meta) (ctx : extraction_ctx) in (* If there is a basename, we use it *) match basename with - | Some basename -> + | Some basename -> ( (* This should be a no-op *) - to_snake_case basename + match !Config.backend with + | Lean -> basename + | FStar | Coq | HOL4 -> to_snake_case basename) | None -> ( (* No basename: we use the first letter of the type *) match ty with |