diff options
| author | Tej Chajed | 2017-02-09 11:15:51 -0500 |
|---|---|---|
| committer | Tej Chajed | 2017-03-14 15:55:00 -0400 |
| commit | 028db341f3cb924c2d1b3a9e0fa5666425130f90 (patch) | |
| tree | 74318bee1763040766c94cecab4848b1b2f84e83 /kernel/nativecode.ml | |
| parent | b54892932959a3b16e31f780f7f1b638062b0a95 (diff) | |
Report missing tactic arguments in error message
Augments "A fully applied tactic is expected" with the list of missing
arguments to the tactic. Addresses [bug
5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions