diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 87dcb1fd..6c523549 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1864,7 +1864,7 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) let body = match !backend with | FStar -> "eval_global " ^ body_name - | Lean -> "eval_global " ^ body_name ^ " (by simp)" + | Lean -> "eval_global " ^ body_name ^ " (by decide)" | Coq -> body_name ^ "%global" | HOL4 -> "get_return_value " ^ body_name in |