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 /vernac/vernacinterp.mli | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Use Evarutil.has_undefined_evars for tactic has_evar.
Diffstat (limited to 'vernac/vernacinterp.mli')
0 files changed, 0 insertions, 0 deletions