Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of inductive types)

2 files changed, 31 insertions, 15 deletions

diff --git a/test-suite/bugs/closed/5755.v b/test-suite/bugs/closed/5755.v
new file mode 100644
index 000000000..e07fdcf83
--- /dev/null
+++ b/test-suite/bugs/closed/5755.v
@@ -0,0 +1,16 @@
+(* Sections taking care of let-ins for inductive types *)
+
+Section Foo.
+
+Inductive foo (A : Type) (x : A) (y := x) (y : A) := Foo.
+
+End Foo.
+
+Section Foo2.
+
+Variable B : Type.
+Variable b : B.
+Let c := b.
+Inductive foo2 (A : Type) (x : A) (y := x) (y : A) := Foo2 : c=c -> foo2 A x y.
+
+End Foo2.
diff --git a/vernac/discharge.ml b/vernac/discharge.ml
index 474c0b4dd..0e4bbd299 100644
--- a/vernac/discharge.ml
+++ b/vernac/discharge.ml
@@ -36,32 +36,32 @@ let detype_param =
      I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
 *)
 
-let abstract_inductive hyps nparams inds =
+let abstract_inductive decls nparamdecls inds =
   let ntyp = List.length inds in
-  let nhyp = Context.Named.length hyps in
-  let args = Context.Named.to_instance mkVar (List.rev hyps) in
+  let ndecls = Context.Named.length decls in
+  let args = Context.Named.to_instance mkVar (List.rev decls) in
   let args = Array.of_list args in
-  let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
+  let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
   let inds' =
     List.map
       (function (tname,arity,template,cnames,lc) ->
 	let lc' = List.map (substl subs) lc in
-	let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
-	let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
+	let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in
+	let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in
         (tname,arity',template,cnames,lc''))
       	inds in
-  let nparams' = nparams + Array.length args in
+  let nparamdecls' = nparamdecls + Array.length args in
 (* To be sure to be the same as before, should probably be moved to process_inductive *)
   let params' = let (_,arity,_,_,_) = List.hd inds' in
-		let (params,_) = decompose_prod_n_assum nparams' arity in
+		let (params,_) = decompose_prod_n_assum nparamdecls' arity in
                 List.map detype_param params
   in
   let ind'' =
   List.map
     (fun (a,arity,template,c,lc) ->
-      let _, short_arity = decompose_prod_n_assum nparams' arity in
+      let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
       let shortlc =
-	List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
+	List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
       { mind_entry_typename = a;
 	mind_entry_arity = short_arity;
 	mind_entry_template = template;
@@ -77,9 +77,9 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
     let ctx = List.rev mip.mind_arity_ctxt in
       mkArity (List.rev ctx, Type ar.template_level), true
 
-let process_inductive (sechyps,_,_ as info) modlist mib =
-  let sechyps = Lib.named_of_variable_context sechyps in
-  let nparams = mib.mind_nparams in
+let process_inductive (section_decls,_,_ as info) modlist mib =
+  let section_decls = Lib.named_of_variable_context section_decls in
+  let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
   let subst, ind_univs =
     match mib.mind_universes with
     | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx
@@ -105,8 +105,8 @@ let process_inductive (sechyps,_,_ as info) modlist mib =
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = Context.Named.map discharge sechyps in
-  let (params',inds') = abstract_inductive sechyps' nparams inds in
+  let section_decls' = Context.Named.map discharge section_decls in
+  let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
   let record = match mib.mind_record with
     | Some (Some (id, _, _)) -> Some (Some id)
     | Some None -> Some None