Merge PR #11544: Cleanup some globref related manipulations

Reviewed-by: herbelin
Reviewed-by: ppedrot

6 files changed, 24 insertions, 25 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/inductiveops.ml b/pretyping/inductiveops.ml
index 36b405e981..816a8c4703 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -28,14 +28,14 @@ open Context.Rel.Declaration
 
 let type_of_inductive env (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
  Inductive.type_of_inductive env (specif,u)
 
 (* Return type as quoted by the user *)
 let type_of_constructor env (cstr,u) =
  let (mib,_ as specif) =
    Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps;
  Inductive.type_of_constructor (cstr,u) specif
 
 (* Return constructor types in user form *)
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
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4582844b71..b4c19775a7 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -27,6 +27,8 @@ open Arguments_renaming
 open Pretype_errors
 open Context.Rel.Declaration
 
+module GR = Names.GlobRef
+
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv
@@ -287,37 +289,36 @@ let judge_of_letin env name defj typj j =
   { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ;
     uj_type = subst1 defj.uj_val j.uj_type }
 
-let check_hyps_inclusion env sigma f x hyps =
+let check_hyps_inclusion env sigma x hyps =
   let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in
-  let f x = EConstr.Unsafe.to_constr (f x) in
-  Typeops.check_hyps_inclusion env ~evars f x hyps
+  Typeops.check_hyps_inclusion env ~evars x hyps
 
 let type_of_constant env sigma (c,u) =
   let open Declarations in
   let cb = Environ.lookup_constant c env in
-  let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in
+  let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in
   let u = EInstance.kind sigma u in
   let ty, csts = Environ.constant_type env (c,u) in
   let sigma = Evd.add_constraints sigma csts in
-  sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c)))
+  sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c)))
 
 let type_of_inductive env sigma (ind,u) =
   let open Declarations in
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-  let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+  let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
   let u = EInstance.kind sigma u in
   let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in
   let sigma = Evd.add_constraints sigma csts in
-  sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind)))
+  sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind)))
 
 let type_of_constructor env sigma ((ind,_ as ctor),u) =
   let open Declarations in
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-  let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in
+  let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
   let u = EInstance.kind sigma u in
   let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
   let sigma = Evd.add_constraints sigma csts in
-  sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor)))
+  sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor)))
 
 let judge_of_int env v =
   Environ.on_judgment EConstr.of_constr (judge_of_int env v)