From 8a382c1906728f89b13d20f541137a670d2c3c75 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Oct 2014 11:31:44 +0200
Subject: Adapting output/Arguments_renaming.out after fixing printing of
 constants which without a @ would have a maximally inserted implicit
 argument.

---
 test-suite/output/Arguments_renaming.out | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index c99dfc0182..dbc1b4a21b 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -6,7 +6,7 @@ The command has indeed failed with message:
 Argument A renamed to T.
 @eq_refl
      : forall (B : Type) (y : B), y = y
-eq_refl
+@eq_refl nat
      : forall x : nat, x = x
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
@@ -63,7 +63,7 @@ The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor 
 myplus is transparent
 Expands to: Constant Top.Test1.myplus
-myplus
+@myplus
      : forall Z : Type, Z -> nat -> nat -> nat
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
-- 
cgit v1.2.3