blob: b262ad718362e8c204416d3cd09a761868dd08ca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
(* $Id$ *)
(*i*)
open Names
(*i*)
(* Universes. *)
type universe = { u_sp : section_path; u_num : int }
val dummy_univ : universe
val prop_univ : universe
val prop_univ_univ : universe
val prop_univ_univ_univ : universe
val new_univ : section_path -> universe
type universes
val initial_universes : universes
val super : universe -> universes -> universe * universes
val sup : universe -> universe -> universes -> universe * universes
exception UniverseInconsistency
type constraint_function =
universe -> universe -> universes -> universes
val enforce_gt : constraint_function
val enforce_geq : constraint_function
val enforce_eq : constraint_function
|
