2 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index be4cd4faea..2066a7ef39 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,3 +46,7 @@ fun x : nat => ifn x is succ n then n else 0
      : bool
 -4
      : Z
+Nil
+     : forall A : Type, list A
+NIL:list nat
+     : list nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 3cc0a189d0..6e637aca39 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -119,3 +119,13 @@ Require Import ZArith.
 Open Scope Z_scope.
 Notation "- 4" := (-2 + -2).
 Check -4.
+
+(**********************************************************************)
+(* Check notations for references with activated or deactivated       *)
+(* implicit arguments                                                 *)
+
+Notation Nil := @nil.
+Check Nil.
+
+Notation NIL := nil.
+Check NIL : list nat.