diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 10 |
1 files changed, 10 insertions, 0 deletions
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 + |