From a913544232062cb6fe0581ede9f07bf9b283eb8d Mon Sep 17 00:00:00 2001
From: Rodolphe Lepigre <rodolphe@bedrocksystems.com>
Date: Tue, 6 Feb 2024 10:16:48 +0100
Subject: [PATCH] Adapt to coq/coq#18546.

---
 src/lean.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lean.ml b/src/lean.ml
index e4fb3c2..8ba6767 100644
--- a/src/lean.ml
+++ b/src/lean.ml
@@ -901,7 +901,7 @@ and declare_def n { ty; body; univs; height } i =
   in
   let () =
     let c = match ref with ConstRef c -> c | _ -> assert false in
-    Global.set_strategy (Evaluable.EvalConstRef c) (Level (-height))
+    Global.set_strategy (Conv_oracle.EvalConstRef c) (Level (-height))
   in
   let inst = { ref; algs } in
   let () = add_declared n i inst in