From c71cff0328fa0ee640f35337278f344e0d00698a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 12:44:59 +0200
Subject: Checker: Report bugfixes from kernel/inductive.ml

Wrong handling of mind_params_ctxt...
---
 checker/inductive.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 59d1a645a5..1c8f570df9 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -104,12 +104,14 @@ let instantiate_params full t u args sign =
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
   let t = mkArity (sign,dummy) in
-    fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+  let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in
+    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) u 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 u params
+		       (subst_instance_context u mib.mind_params_ctxt)
 
 (************************************************************************)
 (************************************************************************)
-- 
cgit v1.2.3