diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-25 17:34:03 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-25 19:06:22 +0200 |
| commit | e8d79faee901881fc08ea31761d530832105eaf7 (patch) | |
| tree | 7cd611e4efb86605f577f6a98932dc14307959ba /tactics/tactic_option.ml | |
| parent | fc4fa4e42289cd13a8732ff2e08bf33ba1708928 (diff) | |
A slightly more fine grained way to check whether a TACTIC EXTEND is global or local to goals.
Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global.
Diffstat (limited to 'tactics/tactic_option.ml')
0 files changed, 0 insertions, 0 deletions