diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index bee8815a2..aa78fbdad 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,27 +36,27 @@ val sort_cmp : val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function -val trans_conv_cmp : conv_pb -> constr trans_conversion_function +val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : - ?evars:(existential->constr option) -> constr trans_conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function val trans_conv_leq : - ?evars:(existential->constr option) -> types trans_conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function -val conv_cmp : conv_pb -> constr conversion_function +val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function val conv : - ?evars:(existential->constr option) -> constr conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function val conv_leq : - ?evars:(existential->constr option) -> types conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function val conv_leq_vecti : - ?evars:(existential->constr option) -> types array conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_default_conv : (conv_pb -> types conversion_function) -> unit -val default_conv : conv_pb -> types conversion_function -val default_conv_leq : types conversion_function +val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit +val default_conv : conv_pb -> ?l2r:bool -> types conversion_function +val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) |