Types inductifs parametriques

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

5 files changed, 32 insertions, 23 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 42e18fadc8..2da3e2cf5d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -220,7 +220,7 @@ let declare_one_elimination ind =
   let env = Global.env () in
   let sigma = Evd.empty in
   let elim_scheme = Indrec.build_indrec env sigma ind in
-  let npars = mip.mind_nparams in
+  let npars = mib.mind_nparams_rec in
   let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in
   let kelim = mip.mind_kelim in
   (* in case the inductive has a type elimination, generates only one
@@ -373,15 +373,15 @@ let interp_mutual lparams lnamearconstrs finite =
 	 in
 
          (* Build the inductive entry *)
-	 { mind_entry_params = params';
-	   mind_entry_typename = name;
+	 { mind_entry_typename = name;
 	   mind_entry_arity = ar;
 	   mind_entry_consnames = constrnames;
 	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
   States.unfreeze fs;
-  notations, { mind_entry_record = false; 
+  notations, { mind_entry_params = params';
+	       mind_entry_record = false; 
 	       mind_entry_finite = finite; 
 	       mind_entry_inds = mispecvec }
   with e -> States.unfreeze fs; raise e
@@ -397,6 +397,7 @@ let declare_mutual_with_eliminations isrecord mie =
 (* Very syntactical equality *)
 let eq_la d1 d2 = match d1,d2 with
   | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') ->
+      (List.length nal = List.length nal') &&
       List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal'
       & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
   | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') ->
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d6eb9cfc50..be815ffd66 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -84,3 +84,5 @@ val admit : unit -> unit
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
+
+
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 8c71c05130..f10a461d6e 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -35,48 +35,54 @@ let detype_param = function
      I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
 *)
 
-let abstract_inductive hyps inds =
+let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in 
   let nhyp = named_context_length hyps in
   let args = instance_from_named_context (List.rev hyps) in
   let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
   let inds' =
     List.map
-      (function (np,tname,arity,cnames,lc) -> 
+      (function (tname,arity,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
-        (np,tname,arity',cnames,lc''))
+        (tname,arity',cnames,lc''))
       	inds in
+  let nparams' = nparams + 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
+		  List.map detype_param params
+  in
+  let ind'' = 
   List.map 
-    (fun (nparams,a,arity,c,lc) ->
-      let nparams' = nparams + Array.length args in
-      let params, short_arity = decompose_prod_n_assum nparams' arity in
+    (fun (a,arity,c,lc) ->
+      let _, 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 detype_param params in
-      { mind_entry_params = params';
-        mind_entry_typename = a;
+	List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
+      { mind_entry_typename = a;
 	mind_entry_arity = short_arity;
 	mind_entry_consnames = c;
 	mind_entry_lc = shortlc })
     inds'
+  in (params',ind'')
+
 
 let process_inductive sechyps modlist mib =
+  let nparams = mib.mind_nparams in
   let inds = 
     array_map_to_list
       (fun mip ->
-	 let nparams = mip.mind_nparams in
 	 let arity = expmod_constr modlist mip.mind_user_arity in
 	 let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
-	 (nparams,
-	  mip.mind_typename,
+	 (mip.mind_typename,
 	  arity,
 	  Array.to_list mip.mind_consnames,
 	  Array.to_list lc))
       mib.mind_packets in
   let sechyps' = map_named_context (expmod_constr modlist) sechyps in
-  let inds' = abstract_inductive sechyps' inds in
+  let (params',inds') = abstract_inductive sechyps' nparams inds in
   { mind_entry_record = mib.mind_record;
     mind_entry_finite = mib.mind_finite;
+    mind_entry_params = params';
     mind_entry_inds = inds' }
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ad41844cea..8b72d5b01d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -586,7 +586,7 @@ let error_bad_induction dep indid kind =
   str "is not allowed"
 
 let error_not_mutual_in_scheme () =
- str "Induction schemes is concerned only with mutually inductive types"
+ str "Induction schemes are concerned only with distinct mutually inductive types"
 
 let explain_inductive_error = function
   (* These are errors related to inductive constructions *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index f6d8b60000..6b412ea681 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -146,7 +146,7 @@ let subst_projection fid l c =
 let declare_projections indsp coers fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let paramdecls = mip.mind_params_ctxt in
+  let paramdecls = mib.mind_params_ctxt in
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
@@ -223,13 +223,13 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let ind = applist (mkRel (1+List.length params+List.length fields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
-    { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_typename = idstruc;
+    { mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] } in
   let mie =
-    { mind_entry_record = true;
+    { mind_entry_params = List.map degenerate_decl params;
+      mind_entry_record = true;
       mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations true mie in