diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
| commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
| tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /test-suite/output/ltac.out | |
| parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) | |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'test-suite/output/ltac.out')
| -rw-r--r-- | test-suite/output/ltac.out | 34 |
1 files changed, 33 insertions, 1 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index d003c70d..1ff09e3a 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,2 +1,34 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Error: +Ltac variable y depends on pattern variable name z which is not bound in current context. +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 (uconstr)", 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 (constr)" and "refine (uconstr)", 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 (constr)", "g1" and "refine (uconstr)", 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 (constr)" and "refine (uconstr)", 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 "h" and "injection (destruction_arg)", last call +failed. +Error: No primitive equality found. +The command has indeed failed with message: +In nested Ltac calls to "h" and "injection (destruction_arg)", last call +failed. +Error: No primitive equality found. +Hx +nat +nat +0 +0 |