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

Instead of various termops and globnames aliases.

2 files changed, 16 insertions, 1 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 15e5c512ed..84eacb196c 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -253,7 +253,7 @@ let mkFloat f = Float f
    least one argument and the function is not itself an applicative
    term *)
 
-let kind c = c
+let kind (c:t) = c
 
 let rec kind_nocast_gen kind c =
   match kind c with
@@ -338,6 +338,19 @@ let isProj c =  match kind c with Proj _ -> true | _ -> false
 let isFix c =  match kind c with Fix _ -> true | _ -> false
 let isCoFix c =  match kind c with CoFix _ -> true | _ -> false
 
+let isRef c = match kind c with
+  | Const _ | Ind _ | Construct _ | Var _ -> true
+  | _ -> false
+
+let isRefX x c =
+  let open GlobRef in
+  match x, kind 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
+
 (* Destructs a de Bruijn index *)
 let destRel c = match kind c with
   | Rel n -> n
diff --git a/kernel/constr.mli b/kernel/constr.mli
index d4af1149c2..159570b5ea 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -256,6 +256,8 @@ val isRel  : constr -> bool
 val isRelN : int -> constr -> bool
 val isVar  : constr -> bool
 val isVarId : Id.t -> constr -> bool
+val isRef : constr -> bool
+val isRefX : GlobRef.t -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool