diff options
| author | coqbot-app[bot] | 2020-10-19 10:45:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-19 10:45:06 +0000 |
| commit | 33f6551fd030643d0accf50dd762bcede5dd4b8b (patch) | |
| tree | 690c39bf35bc3bf460035f2ec0e55df50b859593 /kernel/reduction.mli | |
| parent | 5be9faac2dcf44b383e57f95b4fbd558b8bd24b8 (diff) | |
| parent | 7320cd84f92793572550d1fe1a2181f40466fa81 (diff) | |
Merge PR #13151: Remove the compare_graph field from the conversion API.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 4ae3838691..7d32596f74 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -31,14 +31,12 @@ exception NotConvertible type 'a kernel_conversion_function = env -> 'a -> 'a -> unit type 'a extended_conversion_function = ?l2r:bool -> ?reds:TransparentState.t -> env -> - ?evars:((existential->constr option) * UGraph.t) -> + ?evars:(existential->constr option) -> 'a -> 'a -> unit 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; @@ -50,7 +48,7 @@ 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 -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t +type 'a infer_conversion_function = env -> 'a -> 'a -> Univ.Constraint.t val get_cumulativity_constraints : conv_pb -> Univ.Variance.t array -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t |