Extension de find_inductive aux co-inductifs et renommage en find_rectype

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

3 files changed, 8 insertions, 5 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3fac4eb2f5..02e35d4f2d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -453,7 +453,7 @@ let push_rels vars env =
 
 let descend_then sigma env head dirn =
   let IndType (indf,_) as indt =
-    try find_inductive env sigma (get_type_of env sigma head)
+    try find_rectype env sigma (get_type_of env sigma head)
     with Not_found -> assert false in
   let mispec,_ = dest_ind_family indf in
   let cstr = get_constructors indf in
@@ -490,7 +490,7 @@ let descend_then sigma env head dirn =
 
 let construct_discriminator sigma env dirn c sort =
   let (IndType(IndFamily (mispec,_) as indf,_) as indt) =
-    try find_inductive env sigma (type_of env sigma c)
+    try find_rectype 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 
@@ -523,7 +523,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 IndType (indf,_) =
-	try find_inductive env sigma cty with Not_found -> assert false in
+	try find_rectype env sigma cty with Not_found -> assert false in
       let _,arsort = get_arity env sigma indf in
       let nparams = mis_nparams (fst (dest_ind_family indf)) in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c278e8b971..d7de3df9be 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -337,7 +337,10 @@ let res_case_then gene thin indbinding id status gl =
   let indclause' = clenv_constrain_with_bindings indbinding indclause in
   let newc = clenv_instance_template indclause' in
   let (IndType (indf,realargs) as indt) =
-    find_inductive env sigma (clenv_instance_template_type indclause') in
+    try find_rectype env sigma (clenv_instance_template_type indclause')
+    with Induc ->
+      errorlabstrm "res_case_then"
+	[< 'sTR ("The type of "^(string_of_id id)^" is not inductive") >] in
   let (elim_predicate,neqns) =
     make_inv_predicate env sigma indt id status (pf_concl gl) in
   let (cut_concl,case_tac) =
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 76db1a0b73..281c1eb189 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -184,7 +184,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
 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_inductive env sigma i
+    try find_rectype env sigma i
     with Induc ->
       errorlabstrm "inversion_scheme" (no_inductive_inconstr env i) in
   let (invEnv,invGoal) =