From 81a22cd3bee8fa6144d4eb46128ee8bb287ecb36 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 14:40:36 +0200
Subject: Checker add test for non-trivial constraints

---
 checker/indtypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 2716489a4f..cc3493aa25 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -573,7 +573,7 @@ let check_subtyping mib paramsctxt env_ar inds =
 let check_inductive env kn mib =
   Flags.if_verbose Feedback.msg_notice (str "  checking ind: " ++ MutInd.print kn);
   (* check mind_constraints: should be consistent with env *)
-  let env = Environ.push_context (Univ.instantiate_univ_context mib.mind_universes) env in
+  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)) env in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
-- 
cgit v1.2.3