Types inductifs parametriques

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

4 files changed, 8 insertions, 8 deletions

diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 770f2d6b7e..9d19d37e89 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -127,7 +127,7 @@ let solveLeftBranch rectype g =
   try
     let (lhs,rhs) = match_eqdec_partial (pf_concl g) in
     let (mib,mip) = Global.lookup_inductive rectype in
-    let nparams   = mip.mind_nparams in
+    let nparams   = mib.mind_nparams in
     let getargs l = list_skipn nparams (snd (decompose_app l)) in
     let rargs   = getargs rhs
     and largs   = getargs lhs in 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ef96e5fef..4797146a36 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -393,7 +393,7 @@ let rec build_discriminator sigma env dirn c sort = function
       let (ind,_) = dest_ind_family indf in
       let (mib,mip) = lookup_mind_specif env ind in
       let _,arsort = get_arity env indf in
-      let nparams = mip.mind_nparams  in
+      let nparams = mib.mind_nparams  in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
@@ -673,7 +673,7 @@ let rec build_injrec sigma env dflt c = function
       let cty = type_of env sigma c in
       let (ity,_) = find_mrectype env sigma cty in
       let (mib,mip) = lookup_mind_specif env ity in
-      let nparams = mip.mind_nparams in
+      let nparams = mib.mind_nparams in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
       let newc = mkRel(cnum_nlams-(argnum-nparams)) in
       let (subval,tuplety,dfltval) =
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index dfdacbb99f..c3735b2c8e 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -120,7 +120,7 @@ let match_with_unit_type t =
         let constr_types = mip.mind_nf_lc in 
         let nconstr = Array.length mip.mind_consnames in
         let zero_args c =
-          nb_prod c = mip.mind_nparams in  
+          nb_prod c = mib.mind_nparams in  
 	if nconstr = 1 && array_for_all zero_args constr_types then 
 	  Some hdapp
         else 
@@ -213,11 +213,11 @@ let match_with_nodep_ind t =
       | Ind ind  -> 
           let (mib,mip) = Global.lookup_inductive ind in
 	    if Array.length (mib.mind_packets)>1 then None else
-	      let nodep_constr = has_nodep_prod_after mip.mind_nparams in
+	      let nodep_constr = has_nodep_prod_after mib.mind_nparams in
 		if array_for_all nodep_constr mip.mind_nf_lc then
 		  let params=
 		    if mip.mind_nrealargs=0 then args else
-		      fst (list_chop mip.mind_nparams args) in
+		      fst (list_chop mib.mind_nparams args) in
 		    Some (hdapp,params,mip.mind_nrealargs)
 		else 
 		  None
@@ -233,7 +233,7 @@ let match_with_sigma_type t=
           if (Array.length (mib.mind_packets)=1) &&
 	    (mip.mind_nrealargs=0) &&
 	    (Array.length mip.mind_consnames=1) &&
-	    has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then
+	    has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then
 	      (*allowing only 1 existential*) 
 	      Some (hdapp,args)
 	  else 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e30bb7e63b..29fd46f3e2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -288,7 +288,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
     | _ -> anomaly "compute_construtor_signatures"
   in 
   let (mib,mip) = Global.lookup_inductive ity in
-  let n = mip.mind_nparams in
+  let n = mib.mind_nparams in
   let lc =
     Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in
   let lrecargs = dest_subterms mip.mind_recargs in