From df0d30099a9647e681391c15bac12655819772ce Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Oct 2014 09:01:30 +0200
Subject: Adapting output/Arguments_renaming continued.

---
 test-suite/output/Arguments_renaming.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index dbc1b4a21b..c29f564945 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -103,7 +103,7 @@ The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor 
 myplus is transparent
 Expands to: Constant Top.myplus
-myplus
+@myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 The command has indeed failed with message:
 => Error: All arguments lists must declare the same names.
-- 
cgit v1.2.3