aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/reduction.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-06 19:09:10 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-10-06 20:09:06 +0200
commit84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch)
treebaee8c0b023277d43366996685503c9d1f855413 /kernel/reduction.mli
parentc4db6fc1086d984fd983ff9a6797ad108d220b98 (diff)
Splitting kernel universe code in two modules.
1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.
Diffstat (limited to 'kernel/reduction.mli')
-rw-r--r--kernel/reduction.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ced5c498..a22f3730e 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -30,7 +30,7 @@ exception NotConvertibleVect of int
type 'a conversion_function = env -> 'a -> 'a -> unit
type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function
-type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit
+type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
type 'a trans_universe_conversion_function =
Names.transparent_state -> 'a universe_conversion_function
@@ -47,10 +47,10 @@ type 'a universe_state = 'a * 'a universe_compare
type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
-type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
+type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints
val check_sort_cmp_universes :
- env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit
+ env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit
(* val sort_cmp : *)
(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)