diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 39 |
1 files changed, 30 insertions, 9 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 7c0607cc4d..b9bd41f289 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -13,28 +13,39 @@ open Environ (*********************************************************************** s Reduction functions *) -val whd_betaiotazeta : constr -> constr +val whd_betaiotazeta : env -> constr -> constr val whd_betadeltaiota : env -> constr -> constr val whd_betadeltaiota_nolet : env -> constr -> constr -val whd_betaiota : constr -> constr -val nf_betaiota : constr -> constr +val whd_betaiota : env -> constr -> constr +val nf_betaiota : env -> constr -> constr (*********************************************************************** s conversion functions *) exception NotConvertible exception NotConvertibleVect of int -type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints -type 'a trans_conversion_function = Names.transparent_state -> env -> 'a -> 'a -> Univ.constraints + +type conv_universes = Univ.universes * Univ.constraints option + +type 'a conversion_function = env -> 'a -> 'a -> unit +type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function +type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit +type 'a trans_universe_conversion_function = + Names.transparent_state -> 'a universe_conversion_function + +type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints type conv_pb = CONV | CUMUL -val sort_cmp : - conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints +val sort_cmp_universes : + conv_pb -> sorts -> sorts -> conv_universes -> conv_universes -val conv_sort : sorts conversion_function -val conv_sort_leq : sorts conversion_function +(* val sort_cmp : *) +(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) + +(* val conv_sort : sorts conversion_function *) +(* val conv_sort_leq : sorts conversion_function *) val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -42,6 +53,11 @@ val trans_conv : val trans_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function +val trans_conv_universes : + ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function +val trans_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 @@ -50,6 +66,11 @@ val conv_leq : val conv_leq_vecti : ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function +val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> + ?ts:Names.transparent_state -> constr infer_conversion_function +val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> + ?ts:Names.transparent_state -> types infer_conversion_function + (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function |