From b1eef69751a05eebdbdc9d3091e1dae3386218d0 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 16 Aug 2002 10:00:36 +0000
Subject: Strengthenning rules for modules + No modules in sections

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/inductive.mli | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'kernel/inductive.mli')

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index f279eb79aa..a6ce7d42e8 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -44,8 +44,8 @@ val type_of_constructor  : env -> constructor -> types
 val arities_of_constructors : env -> inductive -> types array
 
 (* Transforms inductive specification into types (in nf) *)
-val arities_of_specif : 
-  kernel_name -> mutual_inductive_body * one_inductive_body -> types array 
+val arities_of_specif : mutual_inductive -> 
+  mutual_inductive_body * one_inductive_body -> types array 
 
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
@@ -62,6 +62,10 @@ val type_case_branches :
    given inductive type. *)
 val check_case_info : env -> inductive -> case_info -> unit
 
+(* Find the ultimate inductive in the mind_equiv chain *)
+
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
 (*s Guard conditions for fix and cofix-points. *)
 val check_fix : env -> fixpoint -> unit
 val check_cofix : env -> cofixpoint -> unit
-- 
cgit v1.2.3