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

10 files changed, 20 insertions, 17 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a3e95abbd8..16139abfeb 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -196,8 +196,8 @@ let lookup_mind_specif ((sp,tyi),args) env =
   { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
     mis_mip = mind_nth_type_packet mib tyi }
 
-let find_inductive env sigma ty =
-  let (mind,largs) = find_minductype env sigma ty in
+let find_rectype env sigma ty =
+  let (mind,largs) = find_mrectype 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/inductive.mli b/kernel/inductive.mli
index 33f85d800b..3033c09a9c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -147,11 +147,11 @@ val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list
 
 val lookup_mind_specif : inductive -> env -> inductive_instance
 
-(* [find_inductive env sigma t] builds an [inductive_type] or raises
-   [Induc] if [t] is not an inductive type; The result is relative to
+(* [find_rectype env sigma t] builds an [inductive_type] or raises
+   [Induc] if [t] is not a (co-)inductive type; The result is relative to
    [env] and [sigma] *)
 
-val find_inductive : env -> 'a evar_map -> constr -> inductive_type
+val find_rectype : env -> 'a evar_map -> constr -> inductive_type
 
 (* [get_constructors indf] build an array of [constructor_summary]
    from some inductive type already analysed as an [inductive_family];
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7edb8680f1..720061fa59 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -209,7 +209,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 -> body_of_type j.uj_type) lfj in
   let indspec =
-    try find_inductive env sigma (body_of_type cj.uj_type)
+    try find_rectype env sigma (body_of_type cj.uj_type)
     with Induc ->
       error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in
   let (bty,rslty) =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 65e4e76ff9..41b9d10695 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -360,7 +360,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 (IndType (indf,realargs) as indt) = 
-    try find_inductive env !isevars (body_of_type cj.uj_type)
+    try find_rectype env !isevars (body_of_type cj.uj_type)
     with Induc -> error_case_not_inductive CCI env
 	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars (body_of_type cj.uj_type)) in
   let pj = match po with
@@ -393,7 +393,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 	      with UserError _ -> findtype (i+1) in
 	    findtype 0 in
 
-  let evalct = find_inductive env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
+  let evalct = find_rectype env !isevars (body_of_type cj.uj_type) (*Pour normaliser evars*)
   and evalPt = nf_ise1 !isevars (body_of_type pj.uj_type) in
 
   let (bty,rsty) =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 9398d40f91..535a0c5836 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -52,8 +52,8 @@ let rec type_of env cstr=
     | IsMutConstruct cstr -> body_of_type (type_of_constructor env sigma cstr)
     | IsMutCase (_,p,c,lf) ->
         let IndType (indf,realargs) =
-          try find_inductive env sigma (type_of env c)
-          with Induc -> anomaly "type_of: Bad inductive" in
+          try find_rectype env sigma (type_of env c)
+          with Induc -> anomaly "type_of: Bad recursive type" in
 	let (aritysign,_) = get_arity env sigma indf in
 	let (psign,_) = splay_prod env sigma (type_of env p) in
         let al =
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5f8d7c2f2c..c045ee73af 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -124,7 +124,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let indspec =
-    try find_inductive env sigma ct
+    try find_rectype env sigma ct
     with Induc -> anomaly "mk_casegoals" in
   let (lbrty,conclty) = type_case_branches env sigma indspec pt p c in
   (acc'',lbrty,conclty)
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) =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 512387d998..413aafce6d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -72,7 +72,7 @@ let explain_case_not_inductive k ctx c ct =
   let pct = prterm_env ctx ct in
   [< 'sTR "In Cases expression, the matched term"; 'bRK(1,1); pc; 'sPC; 
      'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
-     'sTR "which is not an inductive definition" >]
+     'sTR "which is not a (co-)inductive type" >]
   
 let explain_number_branches k ctx c ct expn =
   let pc = prterm_env ctx c in