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

Instead of various termops and globnames aliases.

4 files changed, 12 insertions, 14 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3bd52088c7..c21af82659 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -269,7 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
         let sk2 = Stack.append_app args sk2 in
         lookup_canonical_conversion (proji, Const_cs c2), sk2
       | _ ->
-        let (c2, _) = Termops.global_of_constr sigma t2 in
+        let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
           lookup_canonical_conversion (proji, Const_cs c2),sk2
     with Not_found ->
       let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 3b918b5396..879c007198 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -189,7 +189,7 @@ let rec cs_pattern_of_constr env t =
     let _, params = Inductive.find_rectype env ty in
     Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
-  | _ -> Const_cs (Globnames.global_of_constr t) , None, []
+  | _ -> Const_cs (fst @@ destRef t) , None, []
 
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
@@ -234,7 +234,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
               ((GlobRef.ConstRef proji_sp, (patt, t)),
                { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS })
               :: acc
-            | exception Not_found ->
+            | exception DestKO ->
               if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp);
               acc
           ) acc spopt
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f87c50b5e4..4afed07eda 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1311,11 +1311,9 @@ let reduce_to_ref_gen allow_product env sigma ref t =
           else
             error_cannot_recognize ref
       | _ ->
-          try
-            if GlobRef.equal (fst (global_of_constr sigma c)) ref
-            then it_mkProd_or_LetIn t l
-            else raise Not_found
-          with Not_found ->
+        if isRefX sigma ref c
+        then it_mkProd_or_LetIn t l
+        else
           try
             let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in
             elimrec env t' l
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1541e96635..d5c8c3bd19 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -107,9 +107,9 @@ let class_info env sigma c =
     not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c))
 
 let global_class_of_constr env sigma c =
-  try let gr, u = Termops.global_of_constr sigma c in
+  try let gr, u = EConstr.destRef sigma c in
     GlobRef.Map.find gr !classes, u
-  with Not_found -> not_a_class env sigma c
+  with DestKO | Not_found -> not_a_class env sigma c
 
 let dest_class_app env sigma c =
   let cl, args = EConstr.decompose_app sigma c in
@@ -125,9 +125,9 @@ let class_of_constr env sigma c =
   with e when CErrors.noncritical e -> None
 
 let is_class_constr sigma c =
-  try let gr, u = Termops.global_of_constr sigma c in
+  try let gr, u = EConstr.destRef sigma c in
     GlobRef.Map.mem gr !classes
-  with Not_found -> false
+  with DestKO | Not_found -> false
 
 let rec is_class_type evd c =
   let c, _ = Termops.decompose_app_vect evd c in
@@ -140,9 +140,9 @@ let is_class_evar evd evi =
   is_class_type evd evi.Evd.evar_concl
 
 let is_class_constr sigma c =
-  try let gr, u = Termops.global_of_constr sigma c in
+  try let gr, u = EConstr.destRef sigma c in
     GlobRef.Map.mem gr !classes
-  with Not_found -> false
+  with DestKO | Not_found -> false
 
 let rec is_maybe_class_type evd c =
   let c, _ = Termops.decompose_app_vect evd c in