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

(limited to 'engine/evd.ml')

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