blob: ebb1e1f6794458da0953f49c75ec3bb2699ebf58 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
(* $Id$ *)
(*i*)
open Names
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 : '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
|
