Merge PR #11544: Cleanup some globref related manipulations

Reviewed-by: herbelin
Reviewed-by: ppedrot

6 files changed, 30 insertions, 15 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
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c2cdf98ee8..6c06c1e0f1 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -48,7 +48,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of Id.t * 'constr
+  | ReferenceVariables of Id.t * GlobRef.t
   | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
       * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -182,7 +182,7 @@ let map_ptype_error f = function
 | UnboundVar id -> UnboundVar id
 | NotAType j -> NotAType (on_judgment f j)
 | BadAssumption j -> BadAssumption (on_judgment f j)
-| ReferenceVariables (id, c) -> ReferenceVariables (id, f c)
+| ReferenceVariables (id, c) -> ReferenceVariables (id, c)
 | ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar)
 | CaseNotInductive j -> CaseNotInductive (on_judgment f j)
 | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 0f29717f12..d9842ecefa 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of Id.t * 'constr
+  | ReferenceVariables of Id.t * GlobRef.t
   | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment
       * (Sorts.family * Sorts.family * Sorts.family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -102,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a
 
 val error_assumption : env -> unsafe_judgment -> 'a
 
-val error_reference_variables : env -> Id.t -> constr -> 'a
+val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a
 
 val error_elim_arity :
   env -> pinductive -> constr -> unsafe_judgment ->
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c74bfd0688..2a35f87db8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -116,7 +116,7 @@ let type_of_variable env id =
 (* Checks if a context of variables can be instantiated by the
    variables of the current env.
    Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env ?evars f c sign =
+let check_hyps_inclusion env ?evars c sign =
   let conv env a b = conv env ?evars a b in
   Context.Named.fold_outside
     (fun d1 () ->
@@ -133,7 +133,7 @@ let check_hyps_inclusion env ?evars f c sign =
         | LocalDef _, LocalAssum _ -> raise NotConvertible
         | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1);
       with Not_found | NotConvertible | Option.Heterogeneous ->
-        error_reference_variables env id (f c))
+        error_reference_variables env id c)
     sign
     ~init:()
 
@@ -146,14 +146,14 @@ let check_hyps_inclusion env ?evars f c sign =
 
 let type_of_constant env (kn,_u as cst) =
   let cb = lookup_constant kn env in
-  let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
+  let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in
   let ty, cu = constant_type env cst in
   let () = check_constraints cu env in
     ty
 
 let type_of_constant_in env (kn,_u as cst) =
   let cb = lookup_constant kn env in
-  let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
+  let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in
   constant_type_in env cst
 
 (* Type of a lambda-abstraction. *)
@@ -368,18 +368,18 @@ let check_cast env c ct k expected_type =
    the App case of execute; from this constraints, the expected
    dynamic constraints of the form u<=v are enforced *)
 
-let type_of_inductive_knowing_parameters env (ind,u as indu) args =
+let type_of_inductive_knowing_parameters env (ind,u) args =
   let (mib,_mip) as spec = lookup_mind_specif env ind in
-  check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+  check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
   let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
     env (spec,u) args
   in
   check_constraints cst env;
   t
 
-let type_of_inductive env (ind,u as indu) =
+let type_of_inductive env (ind,u) =
   let (mib,mip) = lookup_mind_specif env ind in
-  check_hyps_inclusion env mkIndU indu mib.mind_hyps;
+  check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
   let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in
   check_constraints cst env;
   t
@@ -390,7 +390,7 @@ let type_of_constructor env (c,_u as cu) =
   let () =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
-    check_hyps_inclusion env mkConstructU cu mib.mind_hyps
+    check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps
   in
   let specif = lookup_mind_specif env (inductive_of_constructor c) in
   let t,cst = constrained_type_of_constructor cu specif in
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index ae816fe26e..f88bc653de 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
 
 (** Check that hyps are included in env and fails with error otherwise *)
 val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
-  ('a -> constr) -> 'a -> Constr.named_context -> unit
+  GlobRef.t -> Constr.named_context -> unit
 
 val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit