Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar.

2 files changed, 4 insertions, 25 deletions

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 ->
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d6cfa3cf9a..790a9e4352 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -873,34 +873,12 @@ TACTIC EXTEND is_evar
     ]
 END
 
-let has_evar sigma c =
-let rec has_evar x =
-  match EConstr.kind sigma x with
-    | Evar _ -> true
-    | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ ->
-      false
-    | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) ->
-      has_evar t1 || has_evar t2
-    | LetIn (_, t1, t2, t3) ->
-      has_evar t1 || has_evar t2 || has_evar t3
-    | App (t1, ts) ->
-      has_evar t1 || has_evar_array ts
-    | Case (_, t1, t2, ts) ->
-      has_evar t1 || has_evar t2 || has_evar_array ts
-    | Fix ((_, tr)) | CoFix ((_, tr)) ->
-      has_evar_prec tr
-    | Proj (p, c) -> has_evar c
-and has_evar_array x =
-  Array.exists has_evar x
-and has_evar_prec (_, ts1, ts2) =
-  Array.exists has_evar ts1 || Array.exists has_evar ts2
-in
-has_evar c
-
 TACTIC EXTEND has_evar
 | [ "has_evar" constr(x) ] -> [
   Proofview.tclEVARMAP >>= fun sigma ->
-  if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars")
+  if Evarutil.has_undefined_evars sigma x
+  then Proofview.tclUNIT ()
+  else Tacticals.New.tclFAIL 0 (str "No evars")
 ]
 END