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

Instead of various termops and globnames aliases.

5 files changed, 24 insertions, 15 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 150dad16c2..e37a58be61 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -119,6 +119,20 @@ let isVarId sigma id c =
 let isRelN sigma n c =
   match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
 
+let isRef sigma c = match kind sigma c with
+  | Const _ | Ind _ | Construct _ | Var _ -> true
+  | _ -> false
+
+let isRefX sigma x c =
+  let open GlobRef in
+  match x, kind sigma c with
+  | ConstRef c, Const (c', _) -> Constant.equal c c'
+  | IndRef i, Ind (i', _) -> eq_ind i i'
+  | ConstructRef i, Construct (i', _) -> eq_constructor i i'
+  | VarRef id, Var id' -> Id.equal id id'
+  | _ -> false
+
+
 let destRel sigma c = match kind sigma c with
 | Rel p -> p
 | _ -> raise DestKO
@@ -723,8 +737,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, t
 
-let is_global sigma gr c =
-  Globnames.is_global gr (to_constr sigma c)
+let is_global = isRefX
 
 module Unsafe =
 struct
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 90f50b764c..181714460d 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -152,6 +152,7 @@ val mkNamedProd_or_LetIn : named_declaration -> types -> types
 val isRel  : Evd.evar_map -> t -> bool
 val isVar  : Evd.evar_map -> t -> bool
 val isInd  : Evd.evar_map -> t -> bool
+val isRef : Evd.evar_map -> t -> bool
 val isEvar : Evd.evar_map -> t -> bool
 val isMeta : Evd.evar_map -> t -> bool
 val isSort : Evd.evar_map -> t -> bool
@@ -175,6 +176,7 @@ val isArity : Evd.evar_map -> t -> bool
 
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
 val isRelN : Evd.evar_map -> int -> t -> bool
+val isRefX : Evd.evar_map -> GlobRef.t -> t -> bool
 
 val destRel : Evd.evar_map -> t -> int
 val destMeta : Evd.evar_map -> t -> metavariable
@@ -319,6 +321,7 @@ val fresh_global :
   Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
 
 val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
+[@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
 (** {5 Extra} *)
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b09cc87f97..8533e05d3e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -555,7 +555,7 @@ let rec check_and_clear_in_constr env evdref err ids global c =
         let () = if global then
           let check id' =
             if Id.Set.mem id' ids then
-              raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c)))
+              raise (ClearDependencyError (id',err,Some (fst @@ destRef c)))
           in
           Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c))
         in
diff --git a/engine/termops.ml b/engine/termops.ml
index a65b8275e6..a5c179bf78 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1066,19 +1066,9 @@ let global_of_constr sigma c =
   | Var id -> VarRef id, EConstr.EInstance.empty
   | _ -> raise Not_found
 
-let is_global sigma c t =
-  let open GlobRef in
-  match c, EConstr.kind sigma t with
-  | ConstRef c, Const (c', _) -> Constant.equal c c'
-  | IndRef i, Ind (i', _) -> eq_ind i i'
-  | ConstructRef i, Construct (i', _) -> eq_constructor i i'
-  | VarRef id, Var id' -> Id.equal id id'
-  | _ -> false
+let is_global = EConstr.isRefX
 
-let isGlobalRef sigma c =
-  match EConstr.kind sigma c with
-  | Const _ | Ind _ | Construct _ | Var _ -> true
-  | _ -> false
+let isGlobalRef = EConstr.isRef
 
 let is_template_polymorphic_ind env sigma f =
   match EConstr.kind sigma f with
diff --git a/engine/termops.mli b/engine/termops.mli
index f970b9ece0..7bbf87239d 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -264,10 +264,13 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
 val is_section_variable : Id.t -> bool
 
 val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t
+[@@ocaml.deprecated "Use [EConstr.destRef] instead (throws DestKO instead of Not_found)."]
 
 val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
+[@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
 val isGlobalRef : Evd.evar_map -> constr -> bool
+[@@ocaml.deprecated "Use [EConstr.isRef] instead."]
 
 val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool