From f1874a538ef7e5886b72c2ec2ce21b23d05aa8d7 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 30 Aug 1999 13:17:26 +0000
Subject: ajout des inductifs (sans types singletons pour l'instant)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@32 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/indtypes.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 8723ec3c65..ebb1e1f679 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -2,6 +2,8 @@
 (* $Id$ *)
 
 (*i*)
+open Names
+open Term
 open Inductive
 open Environ
 (*i*)
@@ -10,3 +12,11 @@ open Environ
    inductive types are some arities. *)
 
 val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit
+
+val sort_of_arity : 'a unsafe_env -> constr -> sorts
+
+val cci_inductive : 
+  'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> 
+    (identifier * typed_type * identifier list * bool * bool * constr) list ->
+      mutual_inductive_body
+
-- 
cgit v1.2.3