blob: 421bc937c8a37c5d4cf4dd406b1b1bdbd3598b00 (
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 : env -> mutual_inductive_entry -> unit
val sort_of_arity : env -> constr -> sorts
val cci_inductive :
env -> env -> path_kind -> int -> bool ->
(identifier * typed_type * identifier list * bool * bool * constr) list ->
constraints ->
mutual_inductive_body
|
