From 29919b725262dca76708192bde65ce82860747be Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 10 Feb 2020 22:31:55 +0100
Subject: Granting #9516 and #9518 (support for numerals and strings in custom
 entries).

---
 test-suite/output/Notations4.out | 2 ++
 test-suite/output/Notations4.v   | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 807914a671..1c8f237bb8 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,6 +14,8 @@ Entry constr:myconstr is
      : nat
 [<< # 0 >>]
      : option nat
+[2 + 3]
+     : nat
 [1 {f 1}]
      : Expr
 fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 2906698386..4ab800c9ba 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,6 +22,9 @@ Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr a
 Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
 Check [ << # 0 >> ].
 
+Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
+Check [ 2 + 3 ].
+
 End A.
 
 Module B.
-- 
cgit v1.2.3