gistfile1.txt

diff --git a/plugins/syntax/rebind_string_syntax.ml4 b/plugins/syntax/rebind_string_syntax.ml4
new file mode 100644
index 0000000..0d9967b
--- /dev/null
+++ b/plugins/syntax/rebind_string_syntax.ml4
@@ -0,0 +1,35 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Pp
+open Util
+open Names
+open Pcoq
+open Libnames
+open Topconstr
+open Glob_term
+open Coqlib
+open Genarg
+
+open String_syntax
+
+let interp_custom str dloc s =
+  GApp (dloc, GRef (dloc, str),
+    [interp_string dloc s])
+
+let uninterp_custom str r =
+  match r with
+  | GApp (_,GRef (_,k),[a]) when k = str ->
+      uninterp_string a
+  | _ -> None
+
+let register_custom_interp str scope =
+  Notation.declare_string_interpreter scope
+  (Nametab.path_of_global str, [])
+  (*json_path, json_module*)
+  (interp_custom str)
+    ([GRef (dummy_loc,str)],
+    uninterp_custom str, true)
+
+VERNAC COMMAND EXTEND StringNotation
+[ "String Notation" reference(str) ":" ident(scope) ] -> [ register_custom_interp (Nametab.global str) (string_of_id scope) ]
+END
diff --git a/plugins/syntax/string_syntax_plugin.mllib b/plugins/syntax/string_syntax_plugin.mllib
index b108c9e..afa7d44 100644
--- a/plugins/syntax/string_syntax_plugin.mllib
+++ b/plugins/syntax/string_syntax_plugin.mllib
@@ -1,2 +1,3 @@
 String_syntax
 String_syntax_plugin_mod
+Rebind_string_syntax