ReferenceVariables error contains a globref instead of a constr

The previous system was from before globref was in the kernel.

4 files changed, 14 insertions, 14 deletions

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