From 30a2f4c5469e25038f5720f03e948519efeef48d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 7 Feb 2020 13:54:23 +0100
Subject: ReferenceVariables error contains a globref instead of a constr

The previous system was from before globref was in the kernel.
---
 kernel/typeops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/typeops.mli')

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
 
-- 
cgit v1.2.3