From 50a39015ea0c86cdb6d368ff7f92ce2091085146 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Nov 2019 07:19:27 +0100
Subject: Fixing a notation printing bug (missing a @ to reflect absence of
 imp. args).

When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
---
 test-suite/output/Notations5.out | 4 ++--
 test-suite/output/Notations5.v   | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out
index 96687ed07f..7afb5ad396 100644
--- a/test-suite/output/Notations5.out
+++ b/test-suite/output/Notations5.out
@@ -104,9 +104,9 @@ u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
 where
 ?A : [ |- Type]
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
-u
+@u
      : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b
 u
      : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b
diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v
index 3c25547aac..92ac4b03ff 100644
--- a/test-suite/output/Notations5.v
+++ b/test-suite/output/Notations5.v
@@ -145,9 +145,9 @@ Module AppliedTermsPrinting.
   Check p.
   (* u *)
   Check @p.
-  (* u -- BUG *)
+  (* @u *)
   Check @u.
-  (* u -- BUG *)
+  (* @u *)
   Check u.
   (* u *)
   Check p 0 0.
-- 
cgit v1.2.3