Merge numeral and string notation plugins

9 files changed, 17 insertions, 44 deletions

diff --git a/plugins/syntax/dune b/plugins/syntax/dune
index 1b3d7598da..f930fc265a 100644
--- a/plugins/syntax/dune
+++ b/plugins/syntax/dune
@@ -1,15 +1,8 @@
 (library
- (name numeral_notation_plugin)
- (public_name coq.plugins.numeral_notation)
- (synopsis "Coq numeral notation plugin")
- (modules g_numeral numeral)
- (libraries coq.vernac))
-
-(library
- (name string_notation_plugin)
- (public_name coq.plugins.string_notation)
- (synopsis "Coq string notation plugin")
- (modules g_string string_notation)
+ (name number_string_notation_plugin)
+ (public_name coq.plugins.number_string_notation)
+ (synopsis "Coq number and string notation plugin")
+ (modules g_number_string string_notation number)
  (libraries coq.vernac))
 
 (library
@@ -26,4 +19,4 @@
  (modules float_syntax)
  (libraries coq.vernac))
 
-(coq.pp (modules g_numeral g_string))
+(coq.pp (modules g_number_string))
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_number_string.mlg
index a3cc786a4a..b584505530 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_number_string.mlg
@@ -8,12 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-DECLARE PLUGIN "numeral_notation_plugin"
+DECLARE PLUGIN "number_string_notation_plugin"
 
 {
 
 open Notation
-open Numeral
+open Number
+open String_notation
 open Pp
 open Names
 open Stdarg
@@ -93,3 +94,9 @@ VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
     { warn_deprecated_numeral_notation ();
       vernac_number_notation (Locality.make_module_locality locality) ty f g [After o] (Id.to_string sc) }
 END
+
+VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
+  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+      ident(sc) ] ->
+    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+END
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
deleted file mode 100644
index 788f9e011d..0000000000
--- a/plugins/syntax/g_string.mlg
+++ /dev/null
@@ -1,25 +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)         *)
-(************************************************************************)
-
-DECLARE PLUGIN "string_notation_plugin"
-
-{
-
-open String_notation
-open Names
-open Stdarg
-
-}
-
-VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) ] ->
-    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
-END
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/number.ml
index 89d757a72a..89d757a72a 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/number.ml
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/number.mli
index 5a13d1068b..5a13d1068b 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/number.mli
diff --git a/plugins/syntax/number_string_notation_plugin.mlpack b/plugins/syntax/number_string_notation_plugin.mlpack
new file mode 100644
index 0000000000..74c32d3a53
--- /dev/null
+++ b/plugins/syntax/number_string_notation_plugin.mlpack
@@ -0,0 +1,3 @@
+Number
+String_notation
+G_number_string
diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack
deleted file mode 100644
index f4d9cae3ff..0000000000
--- a/plugins/syntax/numeral_notation_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-Numeral
-G_numeral
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index dbb0e92d5c..98ea318c92 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Pp
-open Util
 open Names
 open Libnames
 open Constrexpr
diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack
deleted file mode 100644
index 6aa081dab4..0000000000
--- a/plugins/syntax/string_notation_plugin.mlpack
+++ /dev/null
@@ -1,2 +0,0 @@
-String_notation
-G_string