diff options
| author | Son Ho | 2024-04-04 11:56:09 +0200 |
|---|---|---|
| committer | Son Ho | 2024-04-04 11:56:09 +0200 |
| commit | 795e2107e305d425efdf6071b29f186cae83656b (patch) | |
| tree | 8f1cf29f3a25d6e36b323045a1108aef5b50a917 /compiler/ExtractBase.ml | |
| parent | 88cb18c614819f4abba1e0dfdb80c455d334d595 (diff) | |
Update the names of the synthesized backward functions
Diffstat (limited to '')
| -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 74ac9e32..0a7c8df2 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1662,9 +1662,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 |