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 +++
 engine/evd.ml      | 7 +++++++
 engine/evd.mli     | 1 +
 3 files changed, 11 insertions(+)

(limited to 'engine')

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} *)
diff --git a/engine/evd.ml b/engine/evd.ml
index 31c326df6a..eee2cb700c 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1376,6 +1376,13 @@ module MiniEConstr = struct
     in
     UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c
 
+  let to_constr_opt sigma c =
+    let evar_value ev = Some (existential_value sigma ev) in
+    try
+      Some (UnivSubst.nf_evars_and_universes_opt_subst evar_value (universe_subst sigma) c)
+    with NotInstantiatedEvar ->
+      None
+
   let of_named_decl d = d
   let unsafe_to_named_decl d = d
   let of_rel_decl d = d
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