blob: a77cc09217622f442b5d0fe6c9a70694b6d968e5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(* $Id$ *)
(*i*)
open Names
open Univ
open Term
open Inductive
open Environ
(*i*)
(* [mind_check_arities] checks that the types declared for all the
inductive types are some arities. *)
val mind_check_arities : unsafe_env -> mutual_inductive_entry -> unit
val sort_of_arity : unsafe_env -> constr -> sorts
val cci_inductive :
unsafe_env -> unsafe_env -> path_kind -> int -> bool ->
(identifier * typed_type * identifier list * bool * bool * constr) list ->
constraints ->
mutual_inductive_body
|
