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 +-
 test-suite/coqchk/cumulativity.v | 11 ++++++++++-
 2 files changed, 11 insertions(+), 2 deletions(-)

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 *)
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index 3a8f9fa22f..ecf9035bfe 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -49,4 +49,13 @@ Section TpLower.
 
   Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
 
-End TpLower.
\ No newline at end of file
+End TpLower.
+
+
+Section subtyping_test.
+  Universe i j.
+  Constraint i < j.
+
+  Inductive TP2 := tp2 : Type@{i} -> Type@{j} -> TP2.
+
+End subtyping_test.
\ No newline at end of file
-- 
cgit v1.2.3