1 files changed, 0 insertions, 69 deletions
diff --git a/parsing/g_string_syntax.ml b/parsing/g_string_syntax.ml
deleted file mode 100644
index 6a650987..00000000
--- a/parsing/g_string_syntax.ml
+++ /dev/null
@@ -1,69 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id: g_string_syntax.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
-
-open Pp
-open Util
-open Names
-open Pcoq
-open Libnames
-open Topconstr
-open G_ascii_syntax
-open Rawterm
-open Coqlib
-
-exception Non_closed_string
-
-(* make a string term from the string s *)
-
-let string_module = ["Coq";"Strings";"String"]
-
-let string_path = make_path string_module "string"
-
-let string_kn = make_kn string_module "string"
-let static_glob_EmptyString  = ConstructRef ((string_kn,0),1)
-let static_glob_String  = ConstructRef ((string_kn,0),2)
-
-let make_reference id = find_reference "String interpretation" string_module id
-let glob_String = lazy (make_reference "String")
-let glob_EmptyString = lazy (make_reference "EmptyString")
-
-open Lazy
-
-let interp_string dloc s =
-  let le = String.length s in
-  let rec aux n = 
-     if n = le then RRef (dloc, force glob_EmptyString) else
-     RApp (dloc,RRef (dloc, force glob_String),
-       [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
-  in aux 0
-
-let uninterp_string r =
-  try 
-    let b = Buffer.create 16 in
-    let rec aux = function
-    | RApp (_,RRef (_,k),[a;s]) when k = force glob_String ->
-	(match uninterp_ascii a with
-	  | Some c -> Buffer.add_char b (Char.chr c); aux s
-	  | _ -> raise Non_closed_string)
-    | RRef (_,z) when z = force glob_EmptyString ->
-	Some (Buffer.contents b)
-    | _ ->
-	raise Non_closed_string
-    in aux r
-  with 
-   Non_closed_string -> None
-
-let _ =
-  Notation.declare_string_interpreter "string_scope"
-    (string_path,["Coq";"Strings";"String"])
-    interp_string
-    ([RRef (dummy_loc,static_glob_String); 
-      RRef (dummy_loc,static_glob_EmptyString)],
-     uninterp_string, true)