diff options
| author | Son Ho | 2024-03-08 09:42:29 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-08 09:42:29 +0100 |
| commit | 44248ccfe3bfb8c45e5bb434d8dfb3dfa6e6b69c (patch) | |
| tree | dd824e0ac83bb8ee885907615d972b6a522689aa /compiler/Extract.ml | |
| parent | 9d541d1ab6b91e59e4f78f4711af085a33ee4f82 (diff) | |
Update the generation of constant bodies for Lean
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 6c523549..0a21d4ec 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1863,8 +1863,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (fun fmt -> let body = match !backend with - | FStar -> "eval_global " ^ body_name - | Lean -> "eval_global " ^ body_name ^ " (by decide)" + | FStar | Lean -> "eval_global " ^ body_name | Coq -> body_name ^ "%global" | HOL4 -> "get_return_value " ^ body_name in |