diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /pretyping/reductionops.mli | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
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 |