diff options
| author | Jason Gross | 2017-12-12 12:00:25 -0500 |
|---|---|---|
| committer | Jason Gross | 2017-12-14 18:02:41 -0500 |
| commit | 29644bf0814945cbf2b4388b8f8bd19f109503a0 (patch) | |
| tree | ca37a531989f7c329d78dda769f1f54dc7617ea3 /test-suite/output | |
| 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')
| -rw-r--r-- | test-suite/output/bug5778.out | 4 | ||||
| -rw-r--r-- | test-suite/output/bug5778.v | 7 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out new file mode 100644 index 0000000000..91ceb1b583 --- /dev/null +++ b/test-suite/output/bug5778.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call +failed. +The term "I" has type "True" which should be Set, Prop or Type. diff --git a/test-suite/output/bug5778.v b/test-suite/output/bug5778.v new file mode 100644 index 0000000000..0dcd76aeff --- /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. |