From d2c5c5e616a6e118291fe1ce9965c731adac03a8 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 19 Jan 2014 15:09:23 +0100 Subject: Imported Upstream version 8.4pl3dfsg --- test-suite/output/Arguments_renaming.out | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'test-suite/output/Arguments_renaming.out') diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e443115c..17c80d13 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,7 +1,9 @@ The command has indeed failed with message: => Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to B. The command has indeed failed with message: => Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -106,3 +108,6 @@ The command has indeed failed with message: => Error: Argument z cannot be declared implicit. The command has indeed failed with message: => Error: Extra argument y. +The command has indeed failed with message: +=> Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to R. -- cgit v1.2.3