From 39b13903e7a6824f4405f61bb4b41a30cfbd0b3c Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 9 Dec 2015 12:30:32 +0100 Subject: CLEANUP: in the Reduction module --- kernel/reduction.mli | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7db7e57bb..304046a1d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -27,7 +27,7 @@ exception NotConvertible 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 trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function @@ -58,25 +58,14 @@ val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare -val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function -val trans_conv : +val conv : ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function -val trans_conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function -val trans_conv_universes : +val conv_universes : ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val trans_conv_leq_universes : +val conv_leq_universes : ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function -val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function -val conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function -val conv_leq_vecti : - ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function - (** These conversion functions are used by module subtyping, which needs to infer universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> -- cgit v1.2.3