Fix #11738 : Funind using deprecated Coqlib API.

2 files changed, 30 insertions, 43 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")
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f7f8004998..9fa0ec8c08 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -47,18 +47,12 @@ open Context.Rel.Declaration
 
 (* Ugly things which should not be here *)
 
-[@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
-  Coqlib.find_reference "RecursiveDefinition" m s
-
-let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
-let arith_Lt  = ["Coq"; "Arith";"Lt"]
+let coq_constant s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@
+  Coqlib.lib_ref s
 
 let coq_init_constant s =
-  EConstr.of_constr (
-    UnivGen.constr_of_monomorphic_global @@
-    Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
-[@@@ocaml.warning "+3"]
+  EConstr.of_constr(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
@@ -122,26 +116,26 @@ let v_id = Id.of_string "v"
 let def_id = Id.of_string "def"
 let p_id = Id.of_string "p"
 let rec_res_id = Id.of_string "rec_res";;
-let lt = function () -> (coq_init_constant "lt")
-[@@@ocaml.warning "-3"]
-let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le")
-let ex = function () -> (coq_init_constant "ex")
-let nat = function () -> (coq_init_constant "nat")
+let lt = function () -> (coq_init_constant "num.nat.lt")
+let le = function () -> Coqlib.lib_ref "num.nat.le"
+
+let ex = function () -> (coq_init_constant "core.ex.type")
+let nat = function () -> (coq_init_constant "num.nat.type")
 let iter_ref () =
   try find_reference ["Recdef"] "iter"
   with Not_found -> user_err Pp.(str "module Recdef not loaded")
 let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
-let eq = function () -> (coq_init_constant "eq")
+let eq = function () -> (coq_init_constant "core.eq.type")
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
-let le_trans = function () -> (coq_constant arith_Nat "le_trans")
-let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans")
-let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n")
-let le_n = function () -> (coq_init_constant "le_n")
+let le_lt_n_Sm = function () -> (coq_constant "num.nat.le_lt_n_Sm")
+let le_trans = function () -> (coq_constant "num.nat.le_trans")
+let le_lt_trans = function () -> (coq_constant "num.nat.le_lt_trans")
+let lt_S_n = function () -> (coq_constant "num.nat.lt_S_n")
+let le_n = function () -> (coq_init_constant "num.nat.le_n")
 let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_O = function () -> (coq_init_constant "O")
-let coq_S = function () -> (coq_init_constant "S")
-let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
+let coq_O = function () -> (coq_init_constant "num.nat.O")
+let coq_S = function () -> (coq_init_constant"num.nat.S")
+let lt_n_O = function () -> (coq_constant "num.nat.nlt_0_r")
 let max_ref = function () -> (find_reference ["Recdef"] "max")
 let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref))
 
@@ -817,7 +811,7 @@ let rec prove_le g =
         | App (c, [| x0 ; _ |]) ->
           EConstr.isVar sigma x0 &&
           Id.equal (destVar sigma x0) (destVar sigma x) &&
-          EConstr.is_global sigma (le ()) c
+          EConstr.isRefX sigma (le ()) c
         | _ -> false
         in
         let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in
@@ -1194,7 +1188,7 @@ let get_current_subgoals_types pstate =
 exception EmptySubgoals
 let build_and_l sigma l =
   let and_constr =  UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in
-  let conj_constr = Coqlib.build_coq_conj () in
+  let conj_constr = Coqlib.lib_ref "core.and.conj" in
   let mk_and p1 p2 =
     mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in
   let rec is_well_founded t =