diff options
author | Jason Gross <jgross@mit.edu> | 2017-12-12 12:00:25 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-12-14 18:02:41 -0500 |
commit | 29644bf0814945cbf2b4388b8f8bd19f109503a0 (patch) | |
tree | ca37a531989f7c329d78dda769f1f54dc7617ea3 /test-suite/output/bug5778.v | |
parent | b270ad686075e5579dc3826fafdc324ea339785c (diff) |
Make [abstract] nodes show up in the Ltac profile
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
Diffstat (limited to 'test-suite/output/bug5778.v')
-rw-r--r-- | test-suite/output/bug5778.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v new file mode 100644 index 000000000..0dcd76aef --- /dev/null +++ b/test-suite/output/bug5778.v @@ -0,0 +1,7 @@ +Ltac a _ := pose (I : I). +Ltac b _ := a (). +Ltac abs _ := abstract b (). +Ltac c _ := abs (). +Goal True. + Fail c (). +Abort. |