diff options
| -rw-r--r-- | pretyping/evarconv.ml | 12 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 9 |
2 files changed, 21 insertions, 0 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 748143cad5..67d650b112 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1765,3 +1765,15 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = match evar_conv_x flags env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) + +let make_opt = function + | Success evd -> Some evd + | UnifFailure _ -> None + +let conv env ?(ts=default_transparent_state env) evd t1 t2 = + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CONV t1 t2) + +let cumul env ?(ts=default_transparent_state env) evd t1 t2 = + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CUMUL t1 t2) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 0418b352fe..2c4a2f144e 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -35,6 +35,9 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error heuristics ([unify]). *) (** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. + In case the flags are not specified, they default to + [default_flags_of full_transparent_state] currently. + In case of success, the two terms are hence unifiable only if the remaining constraints can be solved or [check_problems_are_solved] is true. @@ -48,6 +51,12 @@ val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_m [@@ocaml.deprecated "Use Evarconv.unify_delay instead"] val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map [@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] +(** The same function resolving evars by side-effect and + catching the exception *) +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining constraints. In case of success the two terms are unified without condition. |