From 3a25b967a944fe37e1ad54e54a904d90311ef381 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Sat, 12 Sep 2020 09:13:44 +0200
Subject: Renaming numnotoption into number_modifier

---
 plugins/syntax/numeral.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 99252484b4..d5fe42b0b4 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -12,8 +12,8 @@ open Libnames
 open Vernacexpr
 open Notation
 
-(** * Numeral notation *)
+(** * Number notation *)
 
-val vernac_numeral_notation : locality_flag ->
-                              qualid -> qualid -> qualid ->
-                              Notation_term.scope_name -> numnot_option -> unit
+val vernac_number_notation : locality_flag ->
+                             qualid -> qualid -> qualid ->
+                             Notation_term.scope_name -> numnot_option -> unit
-- 
cgit v1.2.3


From 11a8997dd8fa83537607272692a3baf10dab342a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:12:00 +0200
Subject: [numeral notation] Adding the via ... using ... option

This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
---
 plugins/syntax/numeral.mli | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

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

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index d5fe42b0b4..1f6896d549 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,6 +14,13 @@ open Notation
 
 (** * Number notation *)
 
+type number_string_via = qualid * (qualid * qualid) list
+type number_option =
+  | After of numnot_option
+  | Via of number_string_via
+
 val vernac_number_notation : locality_flag ->
-                             qualid -> qualid -> qualid ->
-                             Notation_term.scope_name -> numnot_option -> unit
+                             qualid ->
+                             qualid -> qualid ->
+                             number_option list ->
+                             Notation_term.scope_name -> unit
-- 
cgit v1.2.3


From 0520decfdc94d52a2f8658b9cf6a730e6d333f8f Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:23:00 +0200
Subject: [numeral notation] Handle implicit arguments

---
 plugins/syntax/numeral.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 1f6896d549..5a13d1068b 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,7 +14,7 @@ open Notation
 
 (** * Number notation *)
 
-type number_string_via = qualid * (qualid * qualid) list
+type number_string_via = qualid * (bool * qualid * qualid) list
 type number_option =
   | After of numnot_option
   | Via of number_string_via
-- 
cgit v1.2.3


From 3b766fd8859b692e3e93cf83bf87d393e32c572e Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 3 Sep 2020 13:26:00 +0200
Subject: Merge numeral and string notation plugins

---
 plugins/syntax/numeral.mli | 26 --------------------------
 1 file changed, 26 deletions(-)
 delete mode 100644 plugins/syntax/numeral.mli

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

diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
deleted file mode 100644
index 5a13d1068b..0000000000
--- a/plugins/syntax/numeral.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \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 Vernacexpr
-open Notation
-
-(** * Number notation *)
-
-type number_string_via = qualid * (bool * qualid * qualid) list
-type number_option =
-  | After of numnot_option
-  | Via of number_string_via
-
-val vernac_number_notation : locality_flag ->
-                             qualid ->
-                             qualid -> qualid ->
-                             number_option list ->
-                             Notation_term.scope_name -> unit
-- 
cgit v1.2.3