blob: 2104fa721155d354bda071f7eca7545d9f180d6b (
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
37
38
39
40
41
|
(* $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
(*s Graphs of universes. *)
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
(* pretty-printing. *)
val pr_universes : universes -> Pp.std_ppcmds
|
