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.
---
 plugins/syntax/g_numeral.ml4 | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/g_numeral.ml4 b/plugins/syntax/g_numeral.ml4
index a097adec24..fceb0b961f 100644
--- a/plugins/syntax/g_numeral.ml4
+++ b/plugins/syntax/g_numeral.ml4
@@ -66,6 +66,14 @@ let warn_abstract_large_num =
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
       Printer.pr_constant (Global.env ()) f ++ strbrk ".")
 
+let warn_abstract_large_num_no_op =
+  CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
+    (fun f ->
+      strbrk "The 'abstract after' directive has no effect when " ++
+      strbrk "the parsing function (" ++
+      Printer.pr_constant (Global.env ()) f ++ strbrk ") targets an " ++
+      strbrk "option type.")
+
 (** Comparing two raw numbers (base 10, big-endian, non-negative).
     A bit nasty, but not critical: only used to decide when a
     number is considered as large (see warnings above). *)
@@ -468,6 +476,9 @@ let vernac_numeral_notation ty f g scope opts =
             num_ty = ty;
             warning = opts }
   in
+  (match opts, to_kind with
+   | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty
+   | _ -> ());
   (* TODO: un hash suffit-il ? *)
   let uid = Marshal.to_string o [] in
   let i = Notation.(
-- 
cgit v1.2.3