From b4e9701b3fbf88a2aa3d1443d622fc90bfc4ae6a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 24 Nov 2017 21:47:49 +0100
Subject: Use Evarutil.has_undefined_evars for tactic has_evar.

---
 API/API.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 1f1b05eadb..7ec3cbee3b 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -3267,6 +3267,7 @@ sig
 
   exception ClearDependencyError of Names.Id.t * clear_dependency_error
   val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
+  val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
   val e_new_evar :
       Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t ->
       ?candidates:EConstr.constr list -> ?store:Evd.Store.t ->
-- 
cgit v1.2.3