From 6a280b70fc66ff0231a9945cc3b3718385d3971c Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 14 Aug 2018 14:04:08 -0400
Subject: Move g_numeral.ml4 to numeral.ml

As per https://github.com/coq/coq/pull/8064#pullrequestreview-145971522
---
 plugins/syntax/numeral.mli | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 plugins/syntax/numeral.mli

(limited to 'plugins/syntax/numeral.mli')

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
new file mode 100644
index 0000000000..2ad3574fe7
--- /dev/null
+++ b/plugins/syntax/numeral.mli
@@ -0,0 +1,21 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Libnames
+open Constrexpr
+
+(** * Numeral notation *)
+
+type numnot_option =
+  | Nop
+  | Warning of raw_natural_number
+  | Abstract of raw_natural_number
+
+val vernac_numeral_notation : qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
-- 
cgit v1.2.3


From e9d44aefa9d6058c72845788745468aa010708b5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Thu, 23 Aug 2018 15:10:58 -0400
Subject: Make Numeral Notation obey Local/Global

Thanks to Emilio and Pierre-Marie Pédrot for pointers.
---
 plugins/syntax/numeral.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax/numeral.mli')

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 2ad3574fe7..83ede6f48f 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -10,6 +10,7 @@
 
 open Libnames
 open Constrexpr
+open Vernacexpr
 
 (** * Numeral notation *)
 
@@ -18,4 +19,4 @@ type numnot_option =
   | Warning of raw_natural_number
   | Abstract of raw_natural_number
 
-val vernac_numeral_notation : qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
+val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
-- 
cgit v1.2.3