Merge numeral and string notation plugins

14 files changed, 21 insertions, 53 deletions

diff --git a/Makefile.common b/Makefile.common
index 29020dc4ad..caf1821ce5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -151,8 +151,7 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
 SYNTAXCMO:=$(addprefix plugins/syntax/, \
 	int63_syntax_plugin.cmo \
 	float_syntax_plugin.cmo \
-	numeral_notation_plugin.cmo \
-	string_notation_plugin.cmo)
+	number_string_notation_plugin.cmo)
 DERIVECMO:=plugins/derive/derive_plugin.cmo
 LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index b7f1e18d2b..92bcd51528 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -538,12 +538,11 @@ let autoloaded_mlgs = [ (* in the order they are loaded by Coq *)
  "plugins/ltac/g_eqdecide.mlg";
  "plugins/ltac/g_tactic.mlg";
  "plugins/ltac/g_ltac.mlg";
- "plugins/syntax/g_string.mlg";
  "plugins/btauto/g_btauto.mlg";
  "plugins/rtauto/g_rtauto.mlg";
  "plugins/cc/g_congruence.mlg";
  "plugins/firstorder/g_ground.mlg";
- "plugins/syntax/g_numeral.mlg";
+ "plugins/syntax/g_number_string.mlg";
 ]
 
 
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
diff --git a/theories/Init/Byte.v b/theories/Init/Byte.v
index 7449b52d76..e03820ef22 100644
--- a/theories/Init/Byte.v
+++ b/theories/Init/Byte.v
@@ -16,7 +16,7 @@ Require Import Coq.Init.Logic.
 Require Import Coq.Init.Specif.
 Require Coq.Init.Nat.
 
-Declare ML Module "string_notation_plugin".
+Declare ML Module "number_string_notation_plugin".
 
 (** We define an inductive for use with the [String Notation] command
     which contains all ascii characters.  We use 256 constructors for
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 0239778bac..9f8a054b5c 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -30,8 +30,6 @@ Require Export Coq.Init.Tauto.
 *)
 Declare ML Module "cc_plugin".
 Declare ML Module "ground_plugin".
-Declare ML Module "numeral_notation_plugin".
-Declare ML Module "string_notation_plugin".
 
 (* Parsing / printing of hexadecimal numbers *)
 Arguments Nat.of_hex_uint d%hex_uint_scope.
diff --git a/theories/dune b/theories/dune
index e7e4ba9981..18e000cfe1 100644
--- a/theories/dune
+++ b/theories/dune
@@ -14,8 +14,7 @@
    coq.plugins.cc
    coq.plugins.firstorder
 
-   coq.plugins.numeral_notation
-   coq.plugins.string_notation
+   coq.plugins.number_string_notation
    coq.plugins.int63_syntax
    coq.plugins.float_syntax