From 7da855f0e3ed56aa9ad9149f6ef95be11f7ec5d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 10:15:38 +0000
Subject: 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
---
 kernel/inductive.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/inductive.mli')

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];
-- 
cgit v1.2.3