From 7320cd84f92793572550d1fe1a2181f40466fa81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 11 Oct 2020 17:50:40 +0200
Subject: Similarly remove the explicit graph argument in the ~evar conversion
 API.

---
 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 87a5666fcc..d381e55dd6 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
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) ->
+val check_hyps_inclusion : env -> ?evars:(existential->constr option) ->
   GlobRef.t -> Constr.named_context -> unit
 
 (** Types for primitives *)
-- 
cgit v1.2.3