From 44248ccfe3bfb8c45e5bb434d8dfb3dfa6e6b69c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 09:42:29 +0100
Subject: Update the generation of constant bodies for Lean

---
 compiler/Extract.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'compiler')

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
-- 
cgit v1.2.3