From 9a99bad924f3c82107a5ecfa7a906988f0f69309 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 30 Oct 2018 18:07:49 +0100
Subject: Check univ instances in Typing.

---
 kernel/typeops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1bb2d3c79c..c8fd83c8a9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -91,7 +91,8 @@ 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 f c sign =
+let check_hyps_inclusion env ?evars f c sign =
+  let conv env a b = conv env ?evars a b in
   Context.Named.fold_outside
     (fun d1 () ->
       let open Context.Named.Declaration in
-- 
cgit v1.2.3