summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml3
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