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 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'pretyping/evarconv.ml')

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