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

1 files changed, 3 insertions, 3 deletions

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];