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

Instead of various termops and globnames aliases.

1 files changed, 4 insertions, 4 deletions

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