diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
| commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
| tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /test-suite/output/ltac.out | |
| parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) | |
Imported Upstream version 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 |