Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`

12 files changed, 183 insertions, 201 deletions

diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index a4a40d3c5a..8c61f4e96b 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -6,6 +6,7 @@ Require Coq.extraction.Extraction.
 
 Require Import Ascii.
 Require Import String.
+Require Import Coq.Strings.Byte.
 
 (**
  * At the moment, Coq's extraction has no way to add extra import
@@ -40,3 +41,22 @@ Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
 Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
 Extract Inlined Constant String.string_dec => "(Prelude.==)".
 Extract Inlined Constant String.eqb => "(Prelude.==)".
+
+(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
+Extract Inductive byte => "Prelude.Char"
+["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
+
+Extract Inlined Constant Byte.eqb => "(Prelude.==)".
+Extract Inlined Constant Byte.byte_eq_dec => "(Prelude.==)".
+Extract Inlined Constant Ascii.ascii_of_byte => "(\x -> x)".
+Extract Inlined Constant Ascii.byte_of_ascii => "(\x -> x)".
+
+(*
+Require Import ExtrHaskellBasic.
+Definition test := "ceci est un test"%string.
+Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)).
+Definition test3 := List.map ascii_of_nat (List.seq 0 256).
+
+Extraction Language Haskell.
+Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect.
+*)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index a2a6a8fe67..f094d4860e 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -12,7 +12,7 @@
 
 Require Coq.extraction.Extraction.
 
-Require Import Ascii String.
+Require Import Ascii String Coq.Strings.Byte.
 
 Extract Inductive ascii => char
 [
@@ -37,7 +37,19 @@ Extract Inlined Constant Ascii.eqb => "(=)".
 
 Extract Inductive string => "char list" [ "[]" "(::)" ].
 
+(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
+Extract Inductive byte => char
+["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
+
+Extract Inlined Constant Byte.eqb => "(=)".
+Extract Inlined Constant Byte.byte_eq_dec => "(=)".
+Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
+Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
+
 (*
 Definition test := "ceci est un test"%string.
-Recursive Extraction test Ascii.zero Ascii.one.
+Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)).
+Definition test3 := List.map ascii_of_nat (List.seq 0 256).
+
+Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect.
 *)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
deleted file mode 100644
index 94255bab6c..0000000000
--- a/plugins/syntax/ascii_syntax.ml
+++ /dev/null
@@ -1,100 +0,0 @@
-(************************************************************************)
-(*         *   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)         *)
-(************************************************************************)
-
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "ascii_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-open Pp
-open CErrors
-open Util
-open Names
-open Glob_term
-open Globnames
-open Coqlib
-
-exception Non_closed_ascii
-
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-let ascii_module = ["Coq";"Strings";"Ascii"]
-let ascii_modpath = MPfile (make_dir ascii_module)
-
-let ascii_path = make_path ascii_module "ascii"
-
-let ascii_label = Label.make "ascii"
-let ascii_kn = MutInd.make2 ascii_modpath ascii_label
-let path_of_Ascii = ((ascii_kn,0),1)
-let static_glob_Ascii  = ConstructRef path_of_Ascii
-
-let glob_Ascii = lazy (lib_ref "plugins.syntax.Ascii")
-
-open Lazy
-
-let interp_ascii ?loc p =
-  let rec aux n p =
-     if Int.equal n 0 then [] else
-     let mp = p mod 2 in
-     (DAst.make ?loc @@ GRef (lib_ref (if Int.equal mp 0 then "core.bool.false" else "core.bool.true"),None))
-     :: (aux (n-1) (p/2)) in
-  DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
-
-let interp_ascii_string ?loc s =
-  let p =
-    if Int.equal (String.length s) 1 then int_of_char s.[0]
-    else
-      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
-      then int_of_string s
-      else
-	user_err ?loc ~hdr:"interp_ascii_string"
-	 (str "Expects a single character or a three-digits ascii code.") in
-  interp_ascii ?loc p
-
-let uninterp_ascii r =
-  let rec uninterp_bool_list n = function
-    | [] when Int.equal n 0 -> 0
-    | r::l when is_gr r (lib_ref "core.bool.true")  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | r::l when is_gr r (lib_ref "core.bool.false") -> 2*(uninterp_bool_list (n-1) l)
-    | _ -> raise Non_closed_ascii in
-  try
-    let aux c = match DAst.get c with
-    | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l
-    | _ -> raise Non_closed_ascii in
-    Some (aux r)
-  with
-   Non_closed_ascii -> None
-
-let make_ascii_string n =
-  if n>=32 && n<=126 then String.make 1 (char_of_int n)
-  else Printf.sprintf "%03d" n
-
-let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let _ =
-  let sc = "char_scope" in
-  register_string_interpretation sc (interp_ascii_string,uninterp_ascii_string);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = sc;
-      pt_interp_info = Uid sc;
-      pt_required = (ascii_path,ascii_module);
-      pt_refs = [static_glob_Ascii];
-      pt_in_match = true }
diff --git a/plugins/syntax/ascii_syntax_plugin.mlpack b/plugins/syntax/ascii_syntax_plugin.mlpack
deleted file mode 100644
index 7b9213a0e2..0000000000
--- a/plugins/syntax/ascii_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Ascii_syntax
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
new file mode 100644
index 0000000000..1e06cd8ddb
--- /dev/null
+++ b/plugins/syntax/g_string.mlg
@@ -0,0 +1,25 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+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/numeral.ml
index 10a0af0b8f..470deb4a60 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -125,7 +125,7 @@ let vernac_numeral_notation local ty f g scope opts =
       | None -> type_error_of g ty true
   in
   let o = { to_kind; to_ty; of_kind; of_ty;
-            num_ty = ty;
+            ty_name = ty;
             warning = opts }
   in
   (match opts, to_kind with
diff --git a/plugins/syntax/plugin_base.dune b/plugins/syntax/plugin_base.dune
index bfdd480fe9..1ab16c700d 100644
--- a/plugins/syntax/plugin_base.dune
+++ b/plugins/syntax/plugin_base.dune
@@ -6,6 +6,13 @@
  (libraries coq.plugins.ltac))
 
 (library
+ (name string_notation_plugin)
+ (public_name coq.plugins.string_notation)
+ (synopsis "Coq string notation plugin")
+ (modules g_string string_notation)
+ (libraries coq.vernac))
+
+(library
  (name r_syntax_plugin)
  (public_name coq.plugins.r_syntax)
  (synopsis "Coq syntax plugin: reals")
@@ -13,23 +20,8 @@
  (libraries coq.vernac))
 
 (library
- (name ascii_syntax_plugin)
- (public_name coq.plugins.ascii_syntax)
- (synopsis "Coq syntax plugin: ASCII")
- (modules ascii_syntax)
- (libraries coq.vernac))
-
-(library
- (name string_syntax_plugin)
- (public_name coq.plugins.string_syntax)
- (synopsis "Coq syntax plugin: strings")
- (modules string_syntax)
- (libraries coq.plugins.ascii_syntax))
-
-(library
  (name int31_syntax_plugin)
  (public_name coq.plugins.int31_syntax)
  (synopsis "Coq syntax plugin: int31")
  (modules int31_syntax)
  (libraries coq.vernac))
-
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
new file mode 100644
index 0000000000..12ee4c6eda
--- /dev/null
+++ b/plugins/syntax/string_notation.ml
@@ -0,0 +1,98 @@
+(************************************************************************)
+(*         *   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 Pp
+open Util
+open Names
+open Libnames
+open Globnames
+open Constrexpr
+open Constrexpr_ops
+open Notation
+
+(** * String notation *)
+
+let get_constructors ind =
+  let mib,oib = Global.lookup_inductive ind in
+  let mc = oib.Declarations.mind_consnames in
+  Array.to_list
+    (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
+
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_option () = qualid_of_ref "core.option.type"
+let q_list () = qualid_of_ref "core.list.type"
+let q_byte () = qualid_of_ref "core.byte.type"
+
+let has_type f ty =
+  let (sigma, env) = Pfedit.get_current_context () in
+  let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
+  try let _ = Constrintern.interp_constr env sigma c in true
+  with Pretype_errors.PretypeError _ -> false
+
+let type_error_to f ty =
+  CErrors.user_err
+    (pr_qualid f ++ str " should go from Byte.byte or (list Byte.byte) to " ++
+     pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ").")
+
+let type_error_of g ty =
+  CErrors.user_err
+    (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
+     str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
+
+let vernac_string_notation local ty f g scope =
+  let app x y = mkAppC (x,[y]) in
+  let cref q = mkRefC q in
+  let cbyte = cref (q_byte ()) in
+  let clist = cref (q_list ()) in
+  let coption = cref (q_option ()) in
+  let opt r = app coption r in
+  let clist_byte = app clist cbyte in
+  let tyc = Smartlocate.global_inductive_with_alias ty in
+  let to_ty = Smartlocate.global_with_alias f in
+  let of_ty = Smartlocate.global_with_alias g in
+  let cty = cref ty in
+  let arrow x y =
+    mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
+  in
+  let constructors = get_constructors tyc in
+  (* Check the type of f *)
+  let to_kind =
+    if has_type f (arrow clist_byte cty) then ListByte, Direct
+    else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option
+    else if has_type f (arrow cbyte cty) then Byte, Direct
+    else if has_type f (arrow cbyte (opt cty)) then Byte, Option
+    else type_error_to f ty
+  in
+  (* Check the type of g *)
+  let of_kind =
+    if has_type g (arrow cty clist_byte) then ListByte, Direct
+    else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option
+    else if has_type g (arrow cty cbyte) then Byte, Direct
+    else if has_type g (arrow cty (opt cbyte)) then Byte, Option
+    else type_error_of g ty
+  in
+  let o = { to_kind = to_kind;
+            to_ty = to_ty;
+            of_kind = of_kind;
+            of_ty = of_ty;
+            ty_name = ty;
+            warning = () }
+  in
+  let i =
+       { pt_local = local;
+         pt_scope = scope;
+         pt_interp_info = StringNotation o;
+         pt_required = Nametab.path_of_global (IndRef tyc),[];
+         pt_refs = constructors;
+         pt_in_match = true }
+  in
+  enable_prim_token_interpretation i
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
new file mode 100644
index 0000000000..9a0174abf2
--- /dev/null
+++ b/plugins/syntax/string_notation.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*         *   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 Vernacexpr
+
+(** * String notation *)
+
+val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit
diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack
new file mode 100644
index 0000000000..6aa081dab4
--- /dev/null
+++ b/plugins/syntax/string_notation_plugin.mlpack
@@ -0,0 +1,2 @@
+String_notation
+G_string
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
deleted file mode 100644
index 59e65a0672..0000000000
--- a/plugins/syntax/string_syntax.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(*         *   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 Names
-open Globnames
-open Ascii_syntax_plugin.Ascii_syntax
-open Glob_term
-open Coqlib
-
-(* Poor's man DECLARE PLUGIN *)
-let __coq_plugin_name = "string_syntax_plugin"
-let () = Mltop.add_known_module __coq_plugin_name
-
-exception Non_closed_string
-
-(* make a string term from the string s *)
-
-let string_module = ["Coq";"Strings";"String"]
-
-let string_modpath = MPfile (make_dir string_module)
-let string_path = make_path string_module "string"
-
-let string_kn = MutInd.make2 string_modpath @@ Label.make "string"
-let static_glob_EmptyString  = ConstructRef ((string_kn,0),1)
-let static_glob_String  = ConstructRef ((string_kn,0),2)
-
-let glob_String = lazy (lib_ref "plugins.syntax.String")
-let glob_EmptyString = lazy (lib_ref "plugins.syntax.EmptyString")
-
-let is_gr c gr = match DAst.get c with
-| GRef (r, _) -> GlobRef.equal r gr
-| _ -> false
-
-open Lazy
-
-let interp_string ?loc s =
-  let le = String.length s in
-  let rec aux n =
-     if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else
-     DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None),
-       [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
-  in aux 0
-
-let uninterp_string (AnyGlobConstr r) =
-  try
-    let b = Buffer.create 16 in
-    let rec aux c = match DAst.get c with
-    | GApp (k,[a;s]) when is_gr k (force glob_String) ->
-	(match uninterp_ascii a with
-	  | Some c -> Buffer.add_char b (Char.chr c); aux s
-	  | _ -> raise Non_closed_string)
-    | GRef (z,_) when GlobRef.equal z (force glob_EmptyString) ->
-	Some (Buffer.contents b)
-    | _ ->
-	raise Non_closed_string
-    in aux r
-  with
-   Non_closed_string -> None
-
-open Notation
-
-let at_declare_ml_module f x =
-  Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name
-
-let _ =
-  let sc = "string_scope" in
-  register_string_interpretation sc (interp_string,uninterp_string);
-  at_declare_ml_module enable_prim_token_interpretation
-    { pt_local = false;
-      pt_scope = sc;
-      pt_interp_info = Uid sc;
-      pt_required = (string_path,["Coq";"Strings";"String"]);
-      pt_refs = [static_glob_String; static_glob_EmptyString];
-      pt_in_match = true }
diff --git a/plugins/syntax/string_syntax_plugin.mlpack b/plugins/syntax/string_syntax_plugin.mlpack
deleted file mode 100644
index 45d6e0fa23..0000000000
--- a/plugins/syntax/string_syntax_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-String_syntax