Merge pull request #16 from rlepigre/br/evaluable_refactoring

Adapt to coq/coq#18546.
SkySkimmer · Apr 3, 2024 · 06d4418 · 06d4418
2 parents 7be3a84 + a913544
commit 06d4418
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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