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/eConstr.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 6532e08e9d..49cbc4d7e5 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -77,6 +77,9 @@ val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
     For getting the evar-normal form of a term with evars see
    {!Evarutil.nf_evar}. *)
 
+val to_constr_opt : Evd.evar_map -> t -> Constr.t option
+(** Same as [to_constr], but returns [None] if some unresolved evars remain *)
+
 val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
 
 (** {5 Constructors} *)
-- 
cgit v1.2.3