Adapt w.r.t. coq/coq#18935.

SkySkimmer · Apr 16, 2024 · 30790b0 · 30790b0
1 parent 06d4418
commit 30790b0
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/lean.ml b/src/lean.ml
@@ -118,10 +118,11 @@ let lean_scheme env ~dep mind u s =
     in
     let sigma, body =
       Indrec.build_induction_scheme env sigma
-        ((mind, 0), u)
+        ((mind, 0), EConstr.EInstance.make u)
         dep
         s'
     in
+    let body = EConstr.Unsafe.to_constr body in
     let uctx = Evd.universe_context_set sigma in
     match s with
     | LSProp ->