diff options
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 |