petit nettoyage de kernel/inductive

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

5 files changed, 10 insertions, 9 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 6e6de2f3b7..ce26640c0d 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -98,7 +98,7 @@ let head_in gls indl t =
       then find_mrectype (pf_env gls) (project gls) t
       else extract_mrectype t
     in List.mem ity indl
-  with Induc -> false
+  with Not_found -> false
        
 let inductive_of_qualid gls qid =
   let c = 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index aea683dc6e..985db43022 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -420,7 +420,7 @@ let descend_then sigma env head dirn =
    giving [True], and all the rest giving False. *)
 
 let construct_discriminator sigma env dirn c sort =
-  let (IndType((ind,_) as indf,_) as indt) =
+  let (IndType(indf,_) as indt) =
     try find_rectype env sigma (type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
@@ -431,6 +431,7 @@ let construct_discriminator sigma env dirn c sort =
       errorlabstrm "Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with 
 		 dependent types") in
+  let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
   let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = 
@@ -453,8 +454,9 @@ let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | ((sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
-      let IndType ((ind,_)as indf,_) =
+      let IndType (indf,_) =
 	try find_rectype env sigma cty with Not_found -> assert false in
+      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
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2a37b3b19b..5dec8457a4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -373,7 +373,7 @@ let res_case_then gene thin indbinding id status gl =
   check_no_metas indclause' ccl;
   let (IndType (indf,realargs) as indt) =
     try find_rectype env sigma ccl
-    with Induc ->
+    with Not_found ->
       errorlabstrm "res_case_then"
 	(str ("The type of "^(string_of_id id)^" is not inductive")) in
   let (elim_predicate,neqns) =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a4ed4f6c58..1344e009b6 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -200,7 +200,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let (env,i) = add_prods_sign env sigma t in
   let ind =
     try find_rectype env sigma i
-    with Induc ->
+    with Not_found ->
       errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) 
   in
   let (invEnv,invGoal) =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 80dad1b6bf..72bf8a076b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -372,7 +372,7 @@ let dyn_intro_move = function
   | l -> bad_tactic_args "intro_move" l
 
 let rec intros_until s g =
-  match pf_lookup_name_as_renamed (pf_hyps g) (pf_concl g) s with
+  match pf_lookup_name_as_renamed (pf_env g) (pf_concl g) s with
     | Some depth -> tclDO depth intro g
     | None -> 
 	try
@@ -383,7 +383,7 @@ let rec intros_until s g =
 	      str " even after head-reduction")
 
 let rec intros_until_n_gen red n g =
-  match pf_lookup_index_as_renamed (pf_concl g) n with
+  match pf_lookup_index_as_renamed (pf_env g) (pf_concl g) n with
     | Some depth -> tclDO depth intro g
     | None ->
       if red then
@@ -1150,8 +1150,7 @@ let rec is_rec_arg env sigma indpath t =
   try
     let (ind_sp,_) = find_mrectype env sigma t in
     path_of_inductive env ind_sp = indpath
-  with Induc -> 
-    false
+  with Not_found -> false
 
 let rec recargs indpath env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with