From 7c7726a798caa6b506a727703de24d2bb5bb3956 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:04:45 +0200
Subject: Univs: bug fix.

Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
---
 pretyping/inductiveops.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 90aa8000a8..cb091f2d6f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -322,7 +322,8 @@ let instantiate_params t args sign =
 let get_constructor ((ind,u as indu),mib,mip,params) j =
   assert (j <= Array.length mip.mind_consnames);
   let typi = mis_nf_constructor_type (indu,mib,mip) j in
-  let typi = instantiate_params typi params mib.mind_params_ctxt in
+  let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let typi = instantiate_params typi params ctx in
   let (args,ccl) = decompose_prod_assum typi in
   let (_,allargs) = decompose_app ccl in
   let vargs = List.skipn (List.length params) allargs in
-- 
cgit v1.2.3