Types inductifs parametriques

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

5 files changed, 16 insertions, 11 deletions

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index d685051e96..71545d966e 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -58,7 +58,7 @@ let rec decompose_term env t=
 	let targs=Array.map (decompose_term env) args in
 	  Array.fold_left (fun s t->Appli (s,t)) tf targs
     | Construct c->
-	let (_,oib)=Global.lookup_inductive (fst c) in
+	let (oib,_)=Global.lookup_inductive (fst c) in
 	let nargs=mis_constructor_nargs_env env c in
 	  Constructor {ci_constr=c;
 		       ci_arity=nargs;
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 0eb35e95b1..55ad52ee20 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -295,8 +295,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in 
-    let npar = mip0.mind_nparams in
-    let epar = push_rel_context mip0.mind_params_ctxt env in
+    let npar = mib.mind_nparams in
+    let epar = push_rel_context mib.mind_params_ctxt env in
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets = 
@@ -358,7 +358,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in 
 	let field_names = 
-	  list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
+	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
 	assert (List.length field_names = List.length typ);
 	let projs = ref Cset.empty in 
 	let mp,d,_ = repr_kn kn in 
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 9dbda969a1..4e256981fc 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -47,7 +47,7 @@ let rec nb_prod_after n c=
 
 let construct_nhyps ind gls =
   let env=pf_env gls in
-  let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in
+  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
   let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let hyp = nb_prod_after nparams in	
     Array.map hyp constr_types
@@ -99,7 +99,7 @@ let rec kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    nb_prod c = mip.mind_nparams in  
+			    nb_prod c = mib.mind_nparams in  
 			    array_exists is_constant mip.mind_nf_lc in 
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5b265ec864..2560b0b820 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1556,7 +1556,7 @@ and mind_ind_info_hyp_constr indf c =
   let env = Global.env() in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
-  let p = mip.mind_nparams in
+  let p = mib.mind_nparams in
   let a = arity_of_constr_of_mind env indf c in
   let lp=ref (get_constructors env indf).(c).cs_args in
   let lr=ref [] in
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index df059677b5..e8f149402d 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -38,6 +38,8 @@ let print_if_verbose s = if !verbose then print_string s;;
 (* Next exception is used only inside print_coq_object and tag_of_string_tag *)
 exception Uninteresting;;
 
+(* NOT USED anymore, we back to the V6 point of view with global parameters 
+
 (* 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, all params are required    *)
@@ -60,6 +62,8 @@ let extract_nparams pack =
   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                                              *)
@@ -392,11 +396,11 @@ let mk_constant_obj id bo ty variables hyps =
          ty,params)
 ;;
 
-let mk_inductive_obj sp packs variables hyps finite =
+let mk_inductive_obj sp packs variables nparams hyps finite =
  let module D = Declarations in
   let hyps = string_list_of_named_context_list hyps in
   let params = filter_params variables hyps in
-  let nparams = extract_nparams packs in
+(*  let nparams = extract_nparams packs in *)
    let tys =
     let tyno = ref (Array.length packs) in
     Array.fold_right
@@ -524,10 +528,11 @@ let print internal glob_ref kind xml_library_root =
         G.lookup_constant kn in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Ln.IndRef (kn,_) ->
-       let {D.mind_packets=packs ;
+       let {D.mind_nparams=nparams;
+	    D.mind_packets=packs ;
             D.mind_hyps=hyps;
             D.mind_finite=finite} = G.lookup_mind kn in
-          Cic2acic.Inductive kn,mk_inductive_obj kn packs variables hyps finite
+          Cic2acic.Inductive kn,mk_inductive_obj kn packs variables nparams hyps finite
     | Ln.ConstructRef _ ->
        Util.anomaly ("print: this should not happen")
   in