petit nettoyage de kernel/inductive

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

2 files changed, 11 insertions, 10 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index be8f142032..a6db1a5ab8 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -137,7 +137,7 @@ let tuple_ref dep n =
 
 let trad_binder avoid nenv = function
   | CC_untyped_binder -> RHole None
-  | CC_typed_binder ty -> Detyping.detype avoid nenv ty
+  | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
 
 let rec push_vars avoid nenv = function
   | [] -> ([],avoid,nenv)
@@ -207,21 +207,22 @@ let rawconstr_of_prog p =
       	let n = List.length l in
       	let cl = List.map (trad avoid nenv) l in
       	let tuple = tuple_ref dep n in
-	let tyl = List.map (Detyping.detype avoid nenv) tyl in
+	let tyl = List.map (Detyping.detype (Global.env()) avoid nenv) tyl in
       	let args = tyl @ cl in
 	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
     | CC_case (ty,b,el) ->
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
-	let ty = Detyping.detype avoid nenv ty in
+	let ty = Detyping.detype (Global.env()) avoid nenv ty in
 	ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl)
 
     | CC_expr c -> 
-	Detyping.detype avoid nenv c
+	Detyping.detype (Global.env()) avoid nenv c
 
     | CC_hole c -> 
-	RCast (dummy_loc, RHole None, Detyping.detype avoid nenv c)
+	RCast (dummy_loc, RHole None,
+               Detyping.detype (Global.env()) avoid nenv c)
 
   in
   trad [] empty_names_context p
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