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

---
 engine/evarutil.mli | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 90c5c3dc0..636472df6 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -21,6 +21,13 @@ val new_meta : unit -> metavariable
 val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
+
+val new_evar_from_context :
+  named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+  ?candidates:constr list -> ?store:Store.t ->
+  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?principal:bool -> types -> evar_map * EConstr.t
+
 val new_evar :
   env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-- 
cgit v1.2.3