From 748fe5960e29a2c80c35b83bb6edfdd0b55bf5e5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 25 Jun 2017 15:46:52 +0200
Subject: Adding intermediate entry point to create an evar in empty
 rel_context.

---
 engine/evarutil.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'engine/evarutil.ml')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e8d184632e..4abfb674ec 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -412,6 +412,14 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
+let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
+  let instance =
+    match filter with
+    | None -> instance
+    | Some filter -> Filter.filter_list filter instance in
+  new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance
+
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
-- 
cgit v1.2.3