diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-05 11:18:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-06 12:21:03 +0200 |
| commit | 47bf10e0216f7736ffe7921ce74d620594bcfcba (patch) | |
| tree | 0b34b459c14519c1a9dc5a08e7bc01ef4c4b2a1c /test-suite/output/ltac.out | |
| parent | c4789644ab4d1a88f1331efb29b69011a30f5eed (diff) | |
About printing of traces of failures while calling ltac code.
An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...
It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.
It got really bad in 8.5 as in:
Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I. (* was referring to tactic name "Top.Top#<>#1" *)
which this commit fixes.
I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.
Eventually, it might be worth that an Ltac expert brainstrom on it!
Diffstat (limited to 'test-suite/output/ltac.out')
| -rw-r--r-- | test-suite/output/ltac.out | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 20e274e25..21a8cf9ed 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -3,3 +3,22 @@ Error: Ltac variable y depends on pattern variable name z which is not bound in Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z +The command has indeed failed with message: +In nested Ltac calls to "g1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "g2", "g1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +In nested Ltac calls to "f2", "f1" and "refine", last call failed. +The term "I" has type "True" while it is expected to have type "False". +The command has indeed failed with message: +Ltac call to "h" failed. +Error: Ltac variable x is bound to I which cannot be coerced to +a declared or quantified hypothesis. +The command has indeed failed with message: +In nested Ltac calls to "h" and "injection", last call failed. +Error: No primitive equality found. |