Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)

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

8 files changed, 15 insertions, 15 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index eb84a2a0f3..ec4dc3cc30 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1152,8 +1152,8 @@ let find_mcoinductype env sigma c =
     | _ -> raise Induc
 
 (* raise Induc if not an inductive type *)
-let try_mutind_of env sigma ty =
-  let (mind,largs) = find_mrectype env sigma ty in
+let find_inductive env sigma ty =
+  let (mind,largs) = find_minductype env sigma ty in
   let mispec = lookup_mind_specif mind env in 
   let nparams = mis_nparams mispec in
   let (params,realargs) = list_chop nparams largs in
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 583a7cf1ff..25adf3b889 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -210,10 +210,10 @@ val find_mrectype     : env -> 'a evar_map -> constr -> inductive * constr list
 val find_minductype   : env -> 'a evar_map -> constr -> inductive * constr list
 val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
 
-(* [try_mutind_of env sigma t] raises [Induc] if [t] is not an inductive type*)
+(* [find_inductive env sigma t] raises [Induc] if [t] is not an inductive type*)
 (* The resulting summary is relative to the current env *)
 open Inductive
-val try_mutind_of : env -> 'a evar_map -> constr -> inductive_summary
+val find_inductive : env -> 'a evar_map -> constr -> inductive_summary
 
 val get_constructors : env -> 'a evar_map -> inductive_summary
       -> constructor_summary array
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c887116351..4a89568dcb 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,7 +319,7 @@ let check_branches_message env sigma (c,ct) (explft,lft) =
 let type_of_case env sigma ci pj cj lfj =
   let lft = Array.map (fun j -> j.uj_type) lfj in
   let indspec =
-    try try_mutind_of env sigma cj.uj_type
+    try find_inductive env sigma cj.uj_type
     with Induc -> error_case_not_inductive CCI env cj.uj_val cj.uj_type in
   let (bty,rslty) =
     type_case_branches env sigma indspec pj.uj_type pj.uj_val cj.uj_val in
diff --git a/library/indrec.ml b/library/indrec.ml
index b764f6cf73..3b02d092c7 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -438,7 +438,7 @@ let type_mutind_rec env sigma indspec pt p c =
 
 let type_rec_branches recursive env sigma ct pt p c =
   try
-    let indspec = try_mutind_of env sigma ct in
+    let indspec = find_inductive env sigma ct in
     if recursive then 
       type_mutind_rec env sigma indspec  pt p c
     else 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fd6a0457d3..2fbfa70f7c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -190,7 +190,7 @@ type 'a pattern_matching_problem =
 (* Utils *)
 
 let to_mutind env sigma t =
-  try IsInd (t,try_mutind_of env sigma t)
+  try IsInd (t,find_inductive env sigma t)
   with Induc -> NotInd t
 
 let type_of_tomatch_type = function
@@ -831,18 +831,18 @@ let coerce_row typing_fun isevars env row tomatch =
 	  (let tyi = inductive_of_rawconstructor c in
 	   try 
 	     let indtyp = inh_coerce_to_ind isevars env j.uj_type tyi in
-	     IsInd (j.uj_type,try_mutind_of env !isevars j.uj_type)
+	     IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
 	 with NotCoercible ->
 	   (* 2 cas : pas le bon inductive ou pas un inductif du tout *)
 	   try
-	     let ind_data = try_mutind_of env !isevars j.uj_type in
+	     let ind_data = find_inductive env !isevars j.uj_type in
 	     error_bad_constructor_loc cloc CCI
 	       (constructor_of_rawconstructor c) ind_data.mind
 	   with Induc ->
 	     error_case_not_inductive_loc
 	       (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type)
       | None -> 
-	  try IsInd (j.uj_type,try_mutind_of env !isevars j.uj_type)
+	  try IsInd (j.uj_type,find_inductive env !isevars j.uj_type)
 	  with Induc -> NotInd (j.uj_type)
   in (j.uj_val,t)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8462a72f62..3401298136 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -397,7 +397,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | ROldCase (loc,isrec,po,c,lf) ->
   let cj = pretype empty_tycon env isevars lvar lmeta c in
   let {mind=mind;params=params;realargs=realargs} =
-    try try_mutind_of env !isevars cj.uj_type
+    try find_inductive env !isevars cj.uj_type
     with Induc -> error_case_not_inductive CCI env
 	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
   let pj = match po with
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 67c1315246..0e61614b3d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -53,7 +53,7 @@ let rec type_of env cstr=
         let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ
     | IsMutCase (_,p,c,lf) ->
         let ind_data =
-          try try_mutind_of env sigma (type_of env c)
+          try find_inductive env sigma (type_of env c)
           with Induc -> anomaly "type_of: Bad inductive" in
 	let (aritysign,_) = get_arity env sigma ind_data in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 02944443ad..5ecf3a39a2 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -450,7 +450,7 @@ let discriminable env sigma t1 t2 =
 let descend_then sigma env head dirn =
   let headj = unsafe_machine env sigma head in
   let indspec =
-    try try_mutind_of env sigma headj.uj_type
+    try find_inductive env sigma headj.uj_type
     with Not_found -> assert false in
   let construct =
     mkMutConstruct (ith_constructor_of_inductive indspec.mind dirn) in
@@ -499,7 +499,7 @@ let descend_then sigma env head dirn =
 
 let construct_discriminator sigma env dirn c sort =
   let indspec =
-    try try_mutind_of env sigma (type_of env sigma c)
+    try find_inductive env sigma (type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
           like T := c : (A:Set)A->T and a discrimination 
@@ -537,7 +537,7 @@ let rec build_discriminator sigma env dirn c sort = function
   | (MutConstruct(sp,cnum),argnum)::l ->
       let cty = type_of env sigma c in
       let indspec =
-	try try_mutind_of env sigma cty with Not_found -> assert false in
+	try find_inductive env sigma cty with Not_found -> assert false in
       let _,arsort = get_arity env sigma indspec in
       let nparams = indspec.Inductive.nparams in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in