From 10a9c492a486fcb884ffeadd1d05ecb0fae90d0f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 17 Jan 2019 10:51:54 +0100
Subject: [EConstr] Expose API to normalize and check if evars are remaining

---
 engine/evd.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/evd.mli')

diff --git a/engine/evd.mli b/engine/evd.mli
index 7560d68805..de73144895 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -689,6 +689,7 @@ module MiniEConstr : sig
   val of_constr_array : Constr.t array -> t array
 
   val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
+  val to_constr_opt : evar_map -> t -> Constr.t option
 
   val unsafe_to_constr : t -> Constr.t
   val unsafe_to_constr_array : t array -> Constr.t array
-- 
cgit v1.2.3