diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 21:47:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 21:52:14 +0100 |
| commit | b4e9701b3fbf88a2aa3d1443d622fc90bfc4ae6a (patch) | |
| tree | ef0ca3a4049e043f6f1df2e70059c7f2cc9d94ef /API | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Use Evarutil.has_undefined_evars for tactic has_evar.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.mli b/API/API.mli index 1f1b05ead..7ec3cbee3 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 -> |