From 960b6d7e17d7a44ad2e058a5b24a2628293408bc Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 24 May 2017 13:56:51 +0200
Subject: Properly instantiate contexts before pushing

---
 checker/indtypes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index cac7e63134..2716489a4f 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -555,8 +555,8 @@ let check_subtyping mib paramsctxt env_ar inds =
   let dosubst = subst_univs_level_constr sbsubst in
   let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
   let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
-  let env = Environ.push_context uctx env_ar in
-  let env = Environ.push_context uctx_other env in
+  let env = Environ.push_context (Univ.instantiate_univ_context uctx) env_ar in
+  let env = Environ.push_context (Univ.instantiate_univ_context uctx_other) env in
   let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env in
   (* process individual inductive types: *)
   Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
-- 
cgit v1.2.3