Standardize constr -> globref operations to use destRef/isRef/isRefX

Instead of various termops and globnames aliases.

4 files changed, 15 insertions, 15 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9195746dc6..9ef5f478d3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
   Proofview.Goal.enter_one begin fun gl ->
   let sigma = project gl in
   let is_global_exists gr c =
-    Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c
+    Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c
   in
   let inccl = Option.is_empty cls in
   let env = Proofview.Goal.env gl in
@@ -1339,11 +1339,11 @@ let inject_if_homogenous_dependent_pair ty =
     let existTconstr = Coqlib.lib_ref    "core.sigT.intro" in
     (* check whether the equality deals with dep pairs or not *)
     let eqTypeDest = fst (decompose_app sigma t) in
-    if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit;
+    if not (isRefX sigma sigTconstr eqTypeDest) then raise Exit;
     let hd1,ar1 = decompose_app_vect sigma t1 and
         hd2,ar2 = decompose_app_vect sigma t2 in
-    if not (Termops.is_global sigma existTconstr hd1) then raise Exit;
-    if not (Termops.is_global sigma existTconstr hd2) then raise Exit;
+    if not (isRefX sigma existTconstr hd1) then raise Exit;
+    if not (isRefX sigma existTconstr hd2) then raise Exit;
     let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
     (* check if the user has declared the dec principle *)
     (* and compare the fst arguments of the dep pair *)
@@ -1692,8 +1692,8 @@ let () =
       optwrite = (:=) regular_subst_tactic }
 
 let restrict_to_eq_and_identity eq = (* compatibility *)
-  if not (is_global (lib_ref "core.eq.type") eq) &&
-    not (is_global (lib_ref "core.identity.type") eq)
+  if not (Constr.isRefX (lib_ref "core.eq.type") eq) &&
+    not (Constr.isRefX (lib_ref "core.identity.type") eq)
   then raise Constr_matching.PatternMatchingFailure
 
 exception FoundHyp of (Id.t * constr * bool)
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index c5ed02e043..5404404af5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -431,10 +431,10 @@ let match_eq sigma eqn (ref, hetero) =
   in
   match EConstr.kind sigma eqn with
   | App (c, [|t; x; y|]) ->
-    if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y)
+    if not hetero && isRefX sigma ref c then PolymorphicLeibnizEq (t, x, y)
     else raise PatternMatchingFailure
   | App (c, [|t; x; t'; x'|]) ->
-    if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x')
+    if hetero && isRefX sigma ref c then HeterogenousEq (t, x, t', x')
     else raise PatternMatchingFailure
   | _ -> raise PatternMatchingFailure
 
@@ -479,9 +479,9 @@ let find_this_eq_data_decompose env sigma eqn =
 
 let match_sigma env sigma ex =
   match EConstr.kind sigma ex with
-  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f ->
+  | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sig.intro") f ->
       build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr)
-  | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f ->
+  | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sigT.intro") f ->
     build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr)
   | _ -> raise PatternMatchingFailure
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2181eb25af..4239fc8bc0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -352,7 +352,7 @@ let dest_nf_eq env sigma t = match EConstr.kind sigma t with
 | App (r, [| t; x; y |]) ->
   let open Reductionops in
   let eq = Coqlib.lib_ref "core.eq.type" in
-  if EConstr.is_global sigma eq r then
+  if isRefX sigma eq r then
     (t, whd_all env sigma x, whd_all env sigma y)
   else user_err Pp.(str "Not an equality.")
 | _ ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 609b752716..2d900a237a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3955,7 +3955,7 @@ let specialize_eqs id =
     match EConstr.kind !evars ty with
     | Prod (na, t, b) ->
         (match EConstr.kind !evars t with
-        | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq ->
+        | App (eq, [| eqty; x; y |]) when isRefX !evars Coqlib.(lib_ref "core.eq.type") eq ->
             let c = if noccur_between !evars 1 (List.length ctx) x then y else x in
             let pt = mkApp (eq, [| eqty; c; c |]) in
             let ind = destInd !evars eq in
@@ -3963,7 +3963,7 @@ let specialize_eqs id =
               if unif (push_rel_context ctx env) evars pt t then
                 aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
               else acc, in_eqs, ctx, ty
-        | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq ->
+        | App (heq, [| eqty; x; eqty'; y |]) when isRefX !evars (Lazy.force coq_heq_ref) heq ->
             let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in
             let pt = mkApp (heq, [| eqt; c; eqt; c |]) in
             let ind = destInd !evars heq in
@@ -4134,8 +4134,8 @@ let compute_elim_sig sigma ?elimc elimt =
       | Some (LocalDef _) -> error_ind_scheme ""
       | Some (LocalAssum (_,ind)) ->
           let indhd,indargs = decompose_app sigma ind in
-          try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) }
-          with e when CErrors.noncritical e ->
+          try {!res with indref = Some (fst (destRef sigma indhd)) }
+          with DestKO ->
             error "Cannot find the inductive type of the inductive scheme."
 
 let compute_scheme_signature evd scheme names_info ind_type_guess =