From 25cab58df1171c9419396342e9ecc3094b74eca5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Feb 2020 21:09:53 +0100
Subject: Revert "Granting #9516 and #9518 (support for numerals and strings in
 custom entries)."

This reverts commit 29919b725262dca76708192bde65ce82860747be.

It was pushed by mistake as part of #11530. Sorry about it.
---
 test-suite/output/Notations4.out | 2 --
 test-suite/output/Notations4.v   | 3 ---
 2 files changed, 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 1c8f237bb8..807914a671 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -14,8 +14,6 @@ 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 4ab800c9ba..2906698386 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -22,9 +22,6 @@ 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