From e07fcc19cf8459ce2ae87d9ccbbc7806a0be576f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 18 Oct 2018 13:21:02 +0200
Subject: Add back the deprecated conv/cumul functions.

---
 pretyping/evarconv.ml  | 12 ++++++++++++
 pretyping/evarconv.mli |  9 +++++++++
 2 files changed, 21 insertions(+)

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.
-- 
cgit v1.2.3