From 63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Feb 2024 23:16:57 +0100
Subject: Start fixing the tests

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

(limited to 'compiler/Extract.ml')

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