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.
---
 kernel/inductive.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4c1614bac1..35b29e73a6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -96,11 +96,11 @@ let full_inductive_instantiate mib u params sign =
   let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
     Vars.subst_instance_context u ar
 
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
-
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+  let inst_ind = constructor_instantiate mind u mib t in
+   instantiate_params true inst_ind params
+		      (Vars.subst_instance_context u mib.mind_params_ctxt)
+		      
 (************************************************************************)
 (************************************************************************)
 
-- 
cgit v1.2.3