blob: 203b0cbc6a5b4edfedc6f1c44c619bbf54c43c07 (
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
|
(* $Id$ *)
open Names
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
type universes
val initial_universes : universes
val super : universe -> universes -> universe * universes
val sup : universe -> universe -> universes -> universe * universes
type constraint_result =
| Consistent of universes
| Inconsistent
type constraint_function =
universe -> universe -> universes -> constraint_result
val enforce_gt : constraint_function
val enforce_geq : constraint_function
val enforce_eq : constraint_function
|
