diff options
| author | Matthieu Sozeau | 2018-10-18 13:21:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:20:07 +0100 |
| commit | e07fcc19cf8459ce2ae87d9ccbbc7806a0be576f (patch) | |
| tree | 46c2c0d8fd9c94e6b4c2d313ffea978c5fc26a48 | |
| parent | e3178fb2de9a84bbcdc90a60cd8f27cd1323eb36 (diff) | |
Add back the deprecated conv/cumul functions.
| -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. |