From a9efa6f9e601cc2bfa1968dca1cdc0d01ebf55e8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 9 Sep 2016 17:09:59 +0200 Subject: Fix output test-suite after commit 0d3c319. --- test-suite/output/ltac.out | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) (limited to 'test-suite/output/ltac.out') diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 21554e9ff..f4254e4e2 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -4,20 +4,25 @@ 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. +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" and "refine", last call failed. +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", "g1" and "refine", last call failed. +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" and "refine", last call failed. +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", last call failed. +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", last call failed. +In nested Ltac calls to "h" and "injection (destruction_arg)", last call +failed. Error: No primitive equality found. -- cgit v1.2.3