petit nettoyage de kernel/inductive

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

1 files changed, 5 insertions, 5 deletions

diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index c23394e8c7..b369bbf311 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1421,7 +1421,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
  let ncti= Array.length(get_constructors env indf) in
- let (ind,_) = indf in
+ let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let ti =(string_of_id mip.mind_typename) in
  let type_arg= targ1 (* List.nth targ (mis_index dmi)*)  in
@@ -1503,13 +1503,13 @@ and  hd_is_mind t ti =
     try (let env = Global.env() in
          let IndType (indf,targ) = find_rectype env Evd.empty t in
 	 let ncti= Array.length(get_constructors env indf) in
-	 let (ind,_) = indf in
+	 let (ind,_) = dest_ind_family indf in
          let (mib,mip) = lookup_mind_specif env ind in
 	 (string_of_id mip.mind_typename) = ti)
     with _ -> false
 and mind_ind_info_hyp_constr indf c =
   let env = Global.env() in
-  let (ind,_) = indf in
+  let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let p = mip.mind_nparams in
   let a = arity_of_constr_of_mind env indf c in
@@ -1539,7 +1539,7 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
  let ncti= Array.length(get_constructors env indf) in
- let (ind,_) = indf in
+ let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let ti =(string_of_id mip.mind_typename) in
  let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
@@ -1589,7 +1589,7 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
  let ncti= Array.length(get_constructors env indf) in
- let (ind,_) = indf in
+ let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
  let ti =(string_of_id mip.mind_typename) in
  let type_arg= targ1(*List.nth targ (mis_index dmi)*) in