diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 4ae3838691..0027b7bf47 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -37,8 +37,6 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = { - compare_graph : 'a -> UGraph.t; (* used for case inversion in reduction *) - (* Might raise NotConvertible *) compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -48,7 +46,7 @@ type 'a universe_compare = { type 'a universe_state = 'a * 'a universe_compare -type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b +type ('a,'b) generic_conversion_function = env -> UGraph.t -> 'b universe_state -> 'a -> 'a -> 'b type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t |