Fix #11738 : Funind using deprecated Coqlib API.

1 files changed, 10 insertions, 17 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 45fafd2872..7d87fc0220 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -92,18 +92,14 @@ let list_union_eq eq_fun l1 l2 =
 let list_add_set_eq eq_fun x l =
   if List.exists (eq_fun x) l then l else x::l
 
-[@@@ocaml.warning "-3"]
-let coq_constant s =
-  UnivGen.constr_of_monomorphic_global @@
-  Coqlib.gen_reference_in_modules "RecursiveDefinition"
-    Coqlib.init_modules s;;
+let coq_constant s = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref s;;
 
 let find_reference sl s =
   let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
   Nametab.locate (make_qualid dp (Id.of_string s))
 
-let eq = lazy(EConstr.of_constr (coq_constant "eq"))
-let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
+let eq = lazy(EConstr.of_constr (coq_constant "core.eq.type"))
+let refl_equal = lazy(EConstr.of_constr (coq_constant "core.eq.refl"))
 
 let with_full_print f a =
   let old_implicit_args = Impargs.is_implicit_args ()
@@ -369,10 +365,10 @@ let do_observe_tac s tac g =
     ignore(Stack.pop debug_queue);
     v
   with reraise ->
-    let reraise = CErrors.push reraise in
+    let reraise = Exninfo.capture reraise in
     if not (Stack.is_empty debug_queue)
     then print_debug_queue true (fst reraise);
-    Util.iraise reraise
+    Exninfo.iraise reraise
 
 let observe_tac s tac g =
   if do_observe ()
@@ -447,14 +443,11 @@ let h_intros l =
 
 let h_id = Id.of_string "h"
 let hrec_id = Id.of_string "hrec"
-let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded")
-let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc")
-let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv")
-
-[@@@ocaml.warning "-3"]
-let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
-    Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof"
-[@@@ocaml.warning "+3"]
+let well_founded = function () -> EConstr.of_constr (coq_constant "core.wf.well_founded")
+let acc_rel = function () -> EConstr.of_constr (coq_constant "core.wf.acc")
+let acc_inv_id = function () -> EConstr.of_constr (coq_constant "core.wf.acc_inv")
+
+let well_founded_ltof () = EConstr.of_constr (coq_constant "num.nat.well_founded_ltof")
 
 let ltof_ref = function  () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")