diff options
| author | Pierre-Marie Pédrot | 2020-09-28 09:54:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-11 17:35:13 +0200 |
| commit | 9a026fcaeb3fa2678b9c93da8204f9f1ddcc0b31 (patch) | |
| tree | 276a153f77e1bda164ad7bbe72bef8b11285d6e2 /kernel/reduction.mli | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Remove the compare_graph field from the conversion API.
We know statically that the first thing the conversion algorithm is going to
do is to get it from the provided function, so we simply explicitly pass it
around.
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 |