diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1df2a73b..d5a84484 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -251,8 +251,6 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit - val is_conv : env -> evar_map -> constr -> constr -> bool val is_conv_leq : env -> evar_map -> constr -> constr -> bool val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool @@ -266,7 +264,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr *) val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool -(** [infer_fconv] Adds necessary universe constraints to the evar map. +(** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. @raises UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. @@ -274,6 +272,20 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> evar_map * bool +(** Conversion with inference of universe constraints *) +val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr -> + evar_map * bool) -> unit +val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> + evar_map * bool + + +(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a +conversion function. Used to pretype vm and native casts. *) +val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state -> + (constr, evar_map) Reduction.generic_conversion_function) -> + ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env -> + evar_map -> constr -> constr -> evar_map * bool + (** {6 Special-Purpose Reduction Functions } *) val whd_meta : evar_map -> constr -> constr |