Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 238 insertions, 172 deletions

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index f9736714fe..d053ed7453 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -45,6 +45,28 @@ let ext_of_tag =
   | Variable  -> "var"
 ;;
 
+(* Internally, for Coq V7, params of inductive types are associated
+   not to the whole block of mutual inductive (as it was in V6) but to
+   each member of the block; but externally, params remain shared by
+   all members in the concrete syntax; the following function checks
+   that the parameters of each inductive of a same block are all the
+   same, then returns this number; it fails otherwise *)
+let extract_nparams pack =
+ let module D = Declarations in
+ let module U = Util in
+ let module S = Sign in
+
+  let {D.mind_nparams=nparams0} = pack.(0) in
+  let arity0 = D.mind_user_arity pack.(0) in
+  let params0 = S.decompose_prod_n_assum nparams0 arity0 in
+  for i = 1 to Array.length pack - 1 do
+    let {D.mind_nparams=nparamsi} = pack.(i) in
+    let arityi = D.mind_user_arity pack.(i) in
+    let paramsi = S.decompose_prod_n_assum nparamsi arityi in
+    if params0 <> paramsi then U.error "Cannot convert a block of inductive definitions with parameters specific to each inductive to a block of mutual inductive definitions with parameters global to the whole block"
+  done;
+  nparams0
+
 (* could_have_namesakes sp = true iff o is an object that could be cooked and *)
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
@@ -598,11 +620,12 @@ let print_mutual_inductive_packet inner_types names env p =
 (*  and   nparams     is the number of "parameters" in the arity of the    *)
 (*                    mutual inductive types                               *)
 (* returns a stream of XML tokens suitable to be pretty printed via Xml.pp *)
-let print_mutual_inductive packs fv hyps nparams env inner_types =
+let print_mutual_inductive packs fv hyps env inner_types =
  let module D = Declarations in
  let module E = Environ in
  let module X = Xml in
  let module N = Names in
+  let nparams = extract_nparams packs in
   let names =
    List.map
     (fun p -> let {D.mind_typename=typename} = p in N.Name(typename))
@@ -698,12 +721,10 @@ let print sp fn =
           | Some c -> print_definition id c typ [] hyps env inner_types
         end
     | T.IndRef (sp,_) ->
-       let {D.mind_packets=packs ; D.mind_nparams=nparams ; D.mind_hyps=hyps} =
-        G.lookup_mind sp
-       in
+       let {D.mind_packets=packs ; D.mind_hyps=hyps} = G.lookup_mind sp in
         let hyps = string_list_of_named_context_list hyps in
          sp,Inductive,
-          print_mutual_inductive packs [] hyps nparams env inner_types
+          print_mutual_inductive packs [] hyps env inner_types
     | T.ConstructRef _
     | T.EvarRef _ ->
        Util.anomaly ("print: this should not happen")
@@ -815,12 +836,11 @@ let print_object lobj id sp dn fv env =
       | "INDUCTIVE" ->
            let
             {D.mind_packets=packs ;
-             D.mind_nparams=nparams ;
              D.mind_hyps = hyps
             } = G.lookup_mind sp
            in
             let hyps = string_list_of_named_context_list hyps in
-             print_mutual_inductive packs fv hyps nparams env inner_types
+             print_mutual_inductive packs fv hyps env inner_types
       | "VARIABLE" ->
           let (_,(varentry,_,_)) = Declare.out_variable lobj in
            begin
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 96eef57001..8be72eb94f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,10 +21,16 @@ let is_defined cb =
 
 let is_opaque cb = cb.const_opaque
 
+(*s Global and local constant declaration. *)
+
 type constant_entry = {
   const_entry_body : constr;
   const_entry_type : constr option }
 
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
 (* Inductive entries *)
 
 type recarg = 
@@ -45,7 +51,8 @@ type one_inductive_body = {
   mind_nrealargs : int;
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
-  mind_finite : bool }
+  mind_finite : bool;
+  mind_nparams : int }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
@@ -53,8 +60,7 @@ type mutual_inductive_body = {
   mind_hyps : named_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
-  mind_singl : constr option;
-  mind_nparams : int }
+  mind_singl : constr option }
 
 let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
 
@@ -68,10 +74,17 @@ let mind_user_arity mip = match mip.mind_user_arity with
 
 (*s Declaration. *)
 
-type mutual_inductive_entry = {
+type one_inductive_entry = {
   mind_entry_nparams : int;
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
+
+type mutual_inductive_entry = {
   mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr list) list}
+  mind_entry_inds : one_inductive_entry list }
 
 let mind_nth_type_packet mib n = mib.mind_packets.(n)
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 0cc927c8ca..e24ac3bdd1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -25,12 +25,16 @@ val is_defined : constant_body -> bool
 
 val is_opaque : constant_body -> bool
 
-(*s Constant declaration. *)
+(*s Global and local constant declaration. *)
 
 type constant_entry = {
   const_entry_body : constr;
   const_entry_type : constr option }
 
+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+
 (*s Inductive types (internal representation). *)
 
 type recarg = 
@@ -56,7 +60,8 @@ type one_inductive_body = {
   mind_nrealargs : int;
   mind_kelim : sorts list;
   mind_listrec : (recarg list) array;
-  mind_finite : bool }
+  mind_finite : bool;
+  mind_nparams : int }
 
 type mutual_inductive_body = {
   mind_kind : path_kind;
@@ -64,8 +69,7 @@ type mutual_inductive_body = {
   mind_hyps : named_context;
   mind_packets : one_inductive_body array;
   mind_constraints : constraints;
-  mind_singl : constr option;
-  mind_nparams : int }
+  mind_singl : constr option }
 
 val mind_type_finite : mutual_inductive_body -> int -> bool
 val mind_user_lc : one_inductive_body -> types array
@@ -76,8 +80,14 @@ val mind_arities_context : mutual_inductive_body -> rel_declaration list
 
 (*s Declaration of inductive types. *)
 
-type mutual_inductive_entry = {
+type one_inductive_entry = {
   mind_entry_nparams : int;
-  mind_entry_finite : bool;
-  mind_entry_inds : (identifier * constr * identifier list * constr list) list}
+  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_typename : identifier;
+  mind_entry_arity : constr;
+  mind_entry_consnames : identifier list;
+  mind_entry_lc : constr list }
 
+type mutual_inductive_entry = {
+  mind_entry_finite : bool;
+  mind_entry_inds : one_inductive_entry list }
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ece400ad16..f10e59c9c7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -59,7 +59,9 @@ let check_constructors_names id =
 let mind_check_names mie =
   let rec check indset cstset = function
     | [] -> ()
-    | (id,_,cl,_)::inds -> 
+    | ind::inds -> 
+	let id = ind.mind_entry_typename in
+	let cl = ind.mind_entry_consnames in
 	if Idset.mem id indset then
 	  raise (InductiveError (SameNamesTypes id))
 	else
@@ -74,35 +76,20 @@ let mind_check_names mie =
 
 let mind_extract_params n c =
   let (l,c') = decompose_prod_n_assum n c in (l,c')
-  
-let extract nparams c =
-  try fst (mind_extract_params nparams c)
-  with UserError _ -> raise (InductiveError BadEntry)
-
-let check_params params params' =
-  if not (params = params') then raise (InductiveError BadEntry)
-
-let mind_extract_and_check_params mie =
-  let nparams = mie.mind_entry_nparams in
-  match mie.mind_entry_inds with
-    | [] -> anomaly "empty inductive types declaration"
-    | (_,ar,_,_)::l -> 
-	let params = extract nparams ar in
-	List.iter (fun (_,c,_,_) -> check_params params (extract nparams c)) l;
-	params
-
-let mind_check_lc params mie =
-  let nparams = List.length params in
-  let check_lc (_,_,_,lc) =
-    List.iter (fun c -> check_params params (extract nparams c)) lc in
-  List.iter check_lc mie.mind_entry_inds
 
 let mind_check_arities env mie =
   let check_arity id c =
     if not (is_arity env Evd.empty c) then 
       raise (InductiveError (NotAnArity id))
   in
-  List.iter (fun (id,ar,_,_) -> check_arity id ar) mie.mind_entry_inds
+  List.iter
+    (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
+    mie.mind_entry_inds
+
+let mind_check_wellformed env mie =
+  if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
+  mind_check_names mie;
+  mind_check_arities env mie
 
 (***********************************************************************)
 
@@ -313,9 +300,9 @@ let is_recursive listind =
   in 
   array_exists one_is_rec
 
-let cci_inductive env env_ar kind nparams finite inds cst =
+let cci_inductive env env_ar kind finite inds cst =
   let ntypes = List.length inds in
-  let one_packet i (id,ar,cnames,issmall,isunit,lc) =
+  let one_packet i (nparams,id,ar,cnames,issmall,isunit,lc) =
     let recargs = listrec_mconstr env_ar ntypes nparams i lc in
     let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in
     let (ar_sign,ar_sort) = splay_arity env Evd.empty (body_of_type ar) in
@@ -340,11 +327,12 @@ let cci_inductive env env_ar kind nparams finite inds cst =
       mind_sort = ar_sort;
       mind_kelim = kelim;
       mind_listrec = recargs;
-      mind_finite = finite }
+      mind_finite = finite;
+      mind_nparams = nparams }
   in
   let ids = 
     List.fold_left 
-      (fun acc (_,ar,_,_,_,lc) -> 
+      (fun acc (_,_,ar,_,_,_,lc) -> 
 	 Idset.union (global_vars_set (body_of_type ar))
 	   (Array.fold_left
 	      (fun acc c -> Idset.union (global_vars_set (body_of_type c)) acc)
@@ -358,5 +346,4 @@ let cci_inductive env env_ar kind nparams finite inds cst =
     mind_hyps = keep_hyps ids (named_context env);
     mind_packets = packets;
     mind_constraints = cst;
-    mind_singl = None;
-    mind_nparams = nparams }
+    mind_singl = None }
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 71041c279e..b8ea65f16e 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -28,39 +28,27 @@ type inductive_error =
   | BadInduction of bool * identifier * sorts
   | NotMutualInScheme
 
-exception InductiveError of inductive_error
-
-(*s The following functions are utility functions to check and to
-  decompose a declaration. *)
-
-(* [mind_check_names] checks the names of an inductive types declaration
-   i.e. that all the types and constructors names are distinct. 
-   It raises an exception [InductiveError _] if it is not the case. *)
-
-val mind_check_names : mutual_inductive_entry -> unit
-
-(* [mind_extract_and_check_params] extracts the parameters of an inductive
-   types declaration. It raises an exception [InductiveError _] if there is
-   not enough abstractions in any of the terms of the field 
-   [mind_entry_inds]. *)
-
-val mind_extract_and_check_params : 
-  mutual_inductive_entry -> Sign.rel_context
+(* [mind_extract_params] extracts the parameters of an inductive
+   type declaration. *)
 
 val mind_extract_params : int -> constr -> Sign.rel_context * constr
 
-val mind_check_lc : Sign.rel_context -> mutual_inductive_entry -> unit
+exception InductiveError of inductive_error
+
+(*s The following function does checks on inductive declarations. *)
 
-(* [mind_check_arities] checks that the types declared for all the
-   inductive types are some arities. *)
+(* [mind_check_wellformed env mie] checks that the types declared for
+   all the inductive types are arities. It checks also that
+   constructor and inductive names altogether are distinct. It raises
+   an exception [InductiveError _] if [mie] is not well-formed *)
 
-val mind_check_arities : env -> mutual_inductive_entry -> unit
+val mind_check_wellformed : env -> mutual_inductive_entry -> unit
 
 (* [cci_inductive] checks positivity and builds an inductive body *)
 
 val cci_inductive : 
-  env -> env -> path_kind -> int -> bool -> 
-   (identifier * types * identifier list * bool * bool * types array)
+  env -> env -> path_kind -> bool -> 
+   (int * identifier * types * identifier list * bool * bool * types array)
       list ->
       constraints ->
       	mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c0e700a130..64968c5098 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -269,6 +269,23 @@ let push_rel_assum = push_rel_or_named_assum push_rel_assum
 let push_rels_with_univ vars env =
   List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
 
+let safe_infer_local_decl env id = function
+  | LocalDef c -> 
+      let (j,cst) = safe_infer env c in
+      (Name id, Some j.uj_val, j.uj_type), cst
+  | LocalAssum c ->
+      let (j,cst) = safe_infer env c in
+      (Name id, None, assumption_of_judgment env Evd.empty j), cst
+
+let safe_infer_local_decls env decls =
+  let rec inferec env = function
+  | (id, d) :: l -> 
+      let env, l, cst1 = inferec env l in
+      let d, cst2 = safe_infer_local_decl env id d in
+      push_rel d env, d :: l, Constraint.union cst1 cst2
+  | [] -> env, [], Constraint.empty in
+  inferec env decls
+
 (* Insertion of constants and parameters in environment. *)
 
 let add_parameter sp t env =
@@ -370,12 +387,9 @@ let is_unit arinfos constrsinfos =
    | [constrinfos] -> is_logic_constr constrinfos && is_logic_arity arinfos
    | _ -> false
 
-let small_unit constrsinfos (env_ar,nparams,ar) =
+let small_unit constrsinfos (env_ar_par,short_arity) =
   let issmall = List.for_all is_small constrsinfos in
-  let arinfos =
-    let (params,a) = mind_extract_params nparams ar in
-    let env_par = push_rels params env_ar in
-    infos_and_sort env_par a in
+  let arinfos = infos_and_sort env_ar_par short_arity in
   let isunit = is_unit arinfos constrsinfos in
   issmall, isunit
 
@@ -386,63 +400,82 @@ let enforce_type_constructor arsort smax cst =
     | Type uc, Type ua -> Constraint.add (ua,Geq,uc) cst
     | _,_ -> cst
 
-let type_one_constructor env_ar nparams arsort c =
-  let infos = 
-    let (params,dc) = mind_extract_params nparams c in
-    let env_par = push_rels params env_ar in
-    infos_and_sort env_par dc 
-  in
-  (* Constructors are typed-checked here *)
-  let (j,cst) = safe_infer_type env_ar c in
+let type_one_constructor env_ar_par params arsort c =
+  let infos = infos_and_sort env_ar_par c in
+
+  (* Each constructor is typed-checked here *)
+  let (j,cst) = safe_infer_type env_ar_par c in
+  let full_cstr_type = it_mkProd_or_LetIn j.utj_val params in
 
   (* If the arity is at some level Type arsort, then the sort of the
      constructor must be below arsort; here we consider constructors with the
      global parameters (which add a priori more constraints on their sort) *)
   let cst2 = enforce_type_constructor arsort j.utj_type cst in
 
-  (infos, j.utj_val, cst2)
+  (infos, full_cstr_type, cst2)
 
-let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,vc) =
-  let arsort = sort_of_arity env_ar ar in
+let infer_constructor_packet env_ar params short_arity arsort vc =
+  let env_ar_par = push_rels params env_ar in
   let (constrsinfos,jlc,cst) = 
     List.fold_right
-      (fun c (infosl,jl,cst) -> 
-	 let (infos,jc,cst') = type_one_constructor env_ar nparams arsort c in
-	 (infos::infosl,jc::jl, Constraint.union cst cst'))
+      (fun c (infosl,l,cst) ->
+	 let (infos,ct,cst') =
+	   type_one_constructor env_ar_par params arsort c in
+	 (infos::infosl,ct::l, Constraint.union cst cst'))
       vc
-      ([],[],Constraint.empty)
-  in
+      ([],[],Constraint.empty) in
   let vc' = Array.of_list jlc in
-  let issmall,isunit = small_unit constrsinfos (env_par,nparams,ar) in
-  let (_,tyar) = lookup_rel_type (ninds+1-i) env_ar in
-  ((id,tyar,cnames,issmall,isunit,vc'), cst)
+  let issmall,isunit = small_unit constrsinfos (env_ar_par,short_arity) in
+  (issmall,isunit,vc', cst)
 
 let add_mind sp mie env =
-  mind_check_names mie;
-  mind_check_arities env mie;
-  let params = mind_extract_and_check_params mie in
-  let nparams = mie.mind_entry_nparams in
-  mind_check_lc params mie;
-  let ninds = List.length mie.mind_entry_inds in
-  let types_sign = 
-    List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds
-  in
-  (* Arities with params are typed-checked here *)
-  let env_arities = push_rels_with_univ types_sign env in
-  let env_params = push_rels params env_arities in
-  let _,inds,cst =
-    List.fold_right
-      (fun ind (i,inds,cst) -> 
-	 let (ind',cst') = 
-	   type_one_inductive i env_arities env_params nparams ninds ind 
+  mind_check_wellformed env mie;
+
+  (* We first type params and arity of each inductive definition *)
+  (* This allows to build the environment of arities and to share *)
+  (* the set of constraints *)
+  let cst, env_arities, rev_params_arity_list =
+    List.fold_left
+      (fun (cst,env_arities,l) ind ->
+         (* Params are typed-checked here *)
+	 let params = ind.mind_entry_params in
+	 let env_params, params, cst1 = safe_infer_local_decls env params in
+         (* Arities (without params) are typed-checked here *)
+	 let arity, cst2 = safe_infer_type env_params ind.mind_entry_arity in
+	 (* We do not need to generate the universe of full_arity; if
+	    later, after the validation of the inductive definition,
+	    full_arity is used as argument or subject to cast, an
+	    upper universe will be generated *)
+	 let id = ind.mind_entry_typename in
+	 let full_arity = it_mkProd_or_LetIn arity.utj_val params in
+	 Constraint.union cst (Constraint.union cst1 cst2),
+	 push_rel_assum (Name id, full_arity) env_arities,
+         (params, id, full_arity, arity.utj_val)::l)
+      (Constraint.empty,env,[])
+      mie.mind_entry_inds in
+
+  let params_arity_list = List.rev rev_params_arity_list in
+
+  (* Now, we type the constructors (without params) *)
+  let inds,cst =
+    List.fold_right2
+      (fun ind (params,id,full_arity,short_arity) (inds,cst) ->
+	 let arsort = sort_of_arity env full_arity in
+	 let lc = ind.mind_entry_lc in
+	 let (issmall,isunit,lc',cst') =
+	   infer_constructor_packet env_arities params short_arity arsort lc
 	 in
-	 (i-1,ind'::inds, Constraint.union cst cst'))
+	 let nparams = ind.mind_entry_nparams in
+	 let consnames = ind.mind_entry_consnames in
+	 let ind' = (nparams,id,full_arity,consnames,issmall,isunit,lc') in
+	 (ind'::inds, Constraint.union cst cst'))
       mie.mind_entry_inds
-      (ninds,[],Constraint.empty) 
-  in
+      params_arity_list
+      ([],Constraint.empty) in
+
+  (* Finally, we build the inductive packet and push it to env *)
   let kind = kind_of_path sp in
-  let mib = 
-    cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst
+  let mib = cci_inductive env env_arities kind mie.mind_entry_finite inds cst
   in
   add_mind sp mib (add_constraints cst env)
     
diff --git a/library/declare.ml b/library/declare.ml
index 305dd815b8..4d76ef8aaa 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -172,36 +172,19 @@ let declare_constant id cd =
 let inductive_names sp mie =
   let names, _ = 
     List.fold_left
-      (fun (names, n) (id,_,cnames,_) ->
+      (fun (names, n) ind ->
 	 let indsp = (sp,n) in
 	 let names, _ =
 	   List.fold_left
 	     (fun (names, p) id ->
 		let sp = Names.make_path (dirpath sp) id CCI in
 		((sp, ConstructRef (indsp,p)) :: names, p+1))
-	     (names, 1) cnames in
-	 let sp = Names.make_path (dirpath sp) id CCI in
+	     (names, 1) ind.mind_entry_consnames in
+	 let sp = Names.make_path (dirpath sp) ind.mind_entry_typename CCI in
 	 ((sp, IndRef indsp) :: names, n+1))
       ([], 0) mie.mind_entry_inds
   in names
 
-let push_inductive_names sp mie =
-  let _ = 
-    List.fold_left
-      (fun n (id,_,cnames,_) ->
-	 let indsp = (sp,n) in
-	 let _ =
-	   List.fold_left
-	     (fun p id ->
-		let sp = Names.make_path (dirpath sp) id CCI in
-		Nametab.push sp (ConstructRef (indsp,p)); (p+1))
-	     1 cnames in
-	 let sp = Names.make_path (dirpath sp) id CCI in
-	 Nametab.push sp (IndRef indsp);
-	 n+1)
-      0 mie.mind_entry_inds
-  in ()
-
 let check_exists_inductive (sp,_) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_inductive"
@@ -230,7 +213,7 @@ let (in_inductive, out_inductive) =
 
 let declare_mind mie =
   let id = match mie.mind_entry_inds with
-    | (id,_,_,_)::_ -> id
+    | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
   let sp = add_leaf id CCI (in_inductive mie) in
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index c22e869430..097a88e5a9 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -85,7 +85,9 @@ let print_mutual sp mib =
   let pk = kind_of_path sp in
   let env = Global.env () in
   let evd = Evd.empty in
-  let {mind_packets=mipv; mind_nparams=nparams} = mib in 
+  let {mind_packets=mipv} = mib in 
+  (* On suppose que tous les inductifs ont les même paramètres *)
+  let nparams = mipv.(0).mind_nparams in
   let (lpars,_) = decomp_n_prod env evd nparams
 		    (body_of_type (mind_user_arity mipv.(0))) in
   let arities = Array.map (fun mip -> (Name mip.mind_typename, None, mip.mind_nf_arity)) mipv in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index caa6d05d67..41085d3508 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -155,13 +155,21 @@ let build_mutual lparams lnamearconstrs finite =
 	 (Environ.push_rel_assum (Name id,p) env, (Name id,p)::params))
       (env0,[]) lparams
   in
+  (* Pour permettre à terme les let-in dans les params *)
+  let params' =
+    List.map (fun (na,p) ->
+		let id = match na with
+		  | Name id -> id
+		  | Anonymous -> anomaly "Unnamed inductive variable"
+		in (id, LocalAssum p)) params
+  in
   let (ind_env,arityl) =
     List.fold_left
       (fun (env,arl) (recname,arityc,_) ->
          let arity = interp_type sigma env_params arityc in
 	 let fullarity = prod_it arity params in
 	 let env' = Environ.push_rel_assum (Name recname,fullarity) env in
-	 (env', (fullarity::arl)))
+	 (env', (arity::arl)))
       (env0,[]) lnamearconstrs
   in
   let ind_env_params = Environ.push_rels_assum params ind_env in
@@ -169,17 +177,16 @@ let build_mutual lparams lnamearconstrs finite =
     List.map2
       (fun ar (name,_,lname_constr) ->
 	 let constrnames, bodies = List.split lname_constr in
-         let constrs =
-	   List.map
-	     (fun c -> prod_it (interp_constr sigma ind_env_params c) params)
-	     bodies
-	 in (name, ar, constrnames, constrs))
+         let constrs = List.map (interp_constr sigma ind_env_params) bodies in
+	 { mind_entry_nparams = nparams;
+	   mind_entry_params = params';
+	   mind_entry_typename = name;
+	   mind_entry_arity = ar;
+	   mind_entry_consnames = constrnames;
+	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
-  let mie = { 
-    mind_entry_nparams = nparams;
-    mind_entry_finite = finite;
-    mind_entry_inds = mispecvec }
+  let mie = { mind_entry_finite = finite; mind_entry_inds = mispecvec }
   in
   let sp = declare_mind mie in
   if is_verbose() then pPNL(minductive_message lrecnames);
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 25b1383c35..b90f7e4935 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -43,21 +43,21 @@ let abstract_inductive ids_to_abs hyps inds =
       list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
     let inds' =
       List.map
-      	(function (tname,arity,cnames,lc) -> 
+      	(function (np,tname,arity,cnames,lc) -> 
 	   let arity' = mkNamedProd id t arity in
 	   let lc' =
 	     List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc
 	   in
-           (tname,arity',cnames,lc'))
+           (np,tname,arity',cnames,lc'))
       	inds
     in 
     (inds',ABSTRACT) in
   let abstract_one_def id c inds =
     List.map
-      (function (tname,arity,cnames,lc) -> 
+      (function (np,tname,arity,cnames,lc) -> 
 	 let arity' = replace_vars [id, c] arity in
 	 let lc' = List.map (replace_vars [id, c]) lc in
-         (tname,arity',cnames,lc'))
+         (np,tname,arity',cnames,lc'))
       inds in
   let abstract_once ((hyps,inds,modl) as sofar) id =
     match hyps with
@@ -73,7 +73,24 @@ let abstract_inductive ids_to_abs hyps inds =
     List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
   let inds'' =
     List.map 
-      (fun (a,b,c,d) -> (a,body_of_type b,c,List.map body_of_type d))
+      (fun (nparams,a,arity,c,lc) ->
+	 let nparams' = nparams + (List.length revmodl) in
+	 let params, short_arity = decompose_prod_n_assum nparams' arity in
+	 let shortlc =
+	   List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
+	 let params' =
+	   List.map 
+	     (function
+		| (Name id,None,p) -> id, LocalAssum p
+		| (Name id,Some p,_) -> id, LocalDef p
+		| (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
+	     params in
+	 { mind_entry_nparams = nparams';
+	   mind_entry_params = params';
+	   mind_entry_typename = a;
+	   mind_entry_arity = short_arity;
+	   mind_entry_consnames = c;
+	   mind_entry_lc = shortlc })
       inds' in
   (inds'', List.rev revmodl)
 
@@ -83,11 +100,14 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   let inds = 
     array_map_to_list
       (fun mip ->
-	 (mip.mind_typename,
-	  expmod_type oldenv modlist (mind_user_arity mip),
+	 let nparams = mip.mind_nparams in
+	 let arity = expmod_type oldenv modlist (mind_user_arity mip) in
+	 let lc = Array.map (expmod_type oldenv modlist) (mind_user_lc mip) in
+	 (nparams,
+	  mip.mind_typename,
+	  arity,
 	  Array.to_list mip.mind_consnames,
-	  Array.to_list
-	    (Array.map (expmod_type oldenv modlist) (mind_user_lc mip))))
+	  Array.to_list lc))
       mib.mind_packets
   in
   let hyps' = map_named_context (expmod_constr oldenv modlist) mib.mind_hyps in
@@ -103,8 +123,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   in
   let indmodifs,cstrmodifs =
     List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in 
-  ({ mind_entry_nparams = mib.mind_nparams + (List.length modl);
-     mind_entry_finite = finite;
+  ({ mind_entry_finite = finite;
      mind_entry_inds = inds' },
    indmodifs,
    List.flatten cstrmodifs)
@@ -116,13 +135,16 @@ let constant_message id =
 
 let inductive_message inds =
   if Options.is_verbose() then 
-    pPNL (hOV 0 
-	    (match inds with
-	       | [] -> assert false
-	       | [(i,_,_,_)] -> [< pr_id i; 'sTR " is discharged." >]
-	       | l -> [< prlist_with_sep pr_coma 
-			   (fun (id,_,_,_) -> pr_id id) l;
-			 'sPC; 'sTR "are discharged.">]))
+    pPNL
+      (hOV 0 
+	 (match inds with
+	    | [] -> assert false
+	    | [ind] ->
+		[< pr_id ind.mind_entry_typename; 'sTR " is discharged." >]
+	    | l ->
+		[< prlist_with_sep pr_coma 
+		     (fun ind -> pr_id ind.mind_entry_typename) l;
+		   'sPC; 'sTR "are discharged.">]))
 
 (* Discharge operations for the various objects of the environment. *)
 
@@ -213,7 +235,7 @@ let process_object oldenv dir sec_sp
 	let mib = Environ.lookup_mind sp oldenv in
 	let strobj =
 	  { s_CONST = info.s_CONST;
-	    s_PARAM = mib.mind_nparams;
+	    s_PARAM = (mind_nth_type_packet mib 0).mind_nparams;
 	    s_PROJ = List.map (option_app (recalc_sp dir)) info.s_PROJ } in
 	((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
 
@@ -254,7 +276,8 @@ let process_operation = function
 let push_inductive_names ccitab sp mie =
   let _,ccitab =
     List.fold_left
-      (fun (n,ccitab) (id,_,cnames,_) ->
+      (fun (n,ccitab) ind ->
+	 let id = ind.mind_entry_typename in
 	 let indsp = (sp,n) in
 	 let _,ccitab =
 	   List.fold_left
@@ -263,7 +286,7 @@ let push_inductive_names ccitab sp mie =
 		 Stringmap.add (string_of_id x) (ConstructRef (indsp,p)) 
 		   ccitab))
 	     (1,Stringmap.add (string_of_id id) (IndRef indsp) ccitab)
-	     cnames in
+	     ind.mind_entry_consnames in
 	 (n+1,ccitab))
       (0,ccitab)
       mie.mind_entry_inds