diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 19:09:10 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-06 20:09:06 +0200 |
commit | 84add29c036735ceacde73ea98a9a5a454a5e3a0 (patch) | |
tree | baee8c0b023277d43366996685503c9d1f855413 /kernel/reduction.mli | |
parent | c4db6fc1086d984fd983ff9a6797ad108d220b98 (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.mli | 6 |
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 *) |