From 2c59d19ad207a6bf193e9f0c9d73258b3133d484 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:58:06 +0200
Subject: Kernel/Checker: Cleanup fixes of substitutions due to let-ins.

Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
---
 checker/inductive.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5d31649737..e3d8dd2060 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -104,14 +104,11 @@ 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
-  let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in
-    subst_instance_context u ar
-
+    fst (destArity (instantiate_params true 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)
+    instantiate_params true inst_ind u params mib.mind_params_ctxt
 
 (************************************************************************)
 (************************************************************************)
-- 
cgit v1.2.3