From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- test-suite/output/ltac.out | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) (limited to 'test-suite/output/ltac.out') 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 -- cgit v1.2.3