diff options
| author | Pierre-Marie Pédrot | 2014-05-23 14:00:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-24 14:34:09 +0200 |
| commit | 6252e413a81cb45a6b1f5f24b25ab1c5ab8d0de6 (patch) | |
| tree | fe101b5f3b52211e8da8fd75765f44170d7632c6 /dev/base_include | |
| parent | 9cef8345e8a25dad2b5e8e7c7525fbf804847a16 (diff) | |
Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole
proof. Indeed, computing an empty list of arguments triggered a
Proofview.Goal.enter, which broke tactics like [shelve_unifiable].
This does not fix this particular tactic though, because the Ltac
interpreter still enters the goal when calling a Ltac reference.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions