From 296ac045fdfe6d6ae4875d7a6c89cad0c64c2e97 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 14 Aug 2018 11:25:19 -0400
Subject: Add a warning about abstract after being a no-op

As per https://github.com/coq/coq/pull/8064#discussion_r209875616

I decided to make it a warning because it seems more flexible that way;
users to are flipping back and forth between option types and not option
types while designing won't have to update their `abstract after`
directives to do so, and users who don't want to allow this can make it an
actual error message.
---
 test-suite/success/NumeralNotations.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v
index 907ec32671..2072fbbf62 100644
--- a/test-suite/success/NumeralNotations.v
+++ b/test-suite/success/NumeralNotations.v
@@ -160,3 +160,18 @@ Module Test9.
     Fail Numeral Notation wuint wrap'' unwrap'' : wuint_scope.
   End with_let.
 End Test9.
+
+Module Test10.
+  (* Test that it is only a warning to add abstract after to an optional parsing function *)
+  Definition to_uint (v : unit) := Nat.to_uint 0.
+  Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end.
+  Definition of_any_uint (v : Decimal.uint) := tt.
+  Delimit Scope unit_scope with unit.
+  Delimit Scope unit2_scope with unit2.
+  Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1).
+  Local Set Warnings Append "+abstract-large-number-no-op".
+  (* Check that there is actually a warning here *)
+  Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1).
+  (* Check that there is no warning here *)
+  Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
+End Test10.
-- 
cgit v1.2.3