blob: 1e675b2c0c7e8ab3e7e05bd24c6ede24e8869618 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* $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 cci_inductive :
env -> env -> path_kind -> int -> bool ->
(identifier * typed_type * identifier list * bool * bool * constr) list ->
constraints ->
mutual_inductive_body
|