1 files changed, 0 insertions, 83 deletions
diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml
deleted file mode 100644
index 944e2338..00000000
--- a/parsing/g_ascii_syntax.ml
+++ /dev/null
@@ -1,83 +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_ascii_syntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
-
-open Pp
-open Util
-open Names
-open Pcoq
-open Rawterm
-open Topconstr
-open Libnames
-open Coqlib
-open Bigint
-
-exception Non_closed_ascii
-
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_kn dir id = Libnames.encode_kn (make_dir dir) (id_of_string id)
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
-
-let ascii_module = ["Coq";"Strings";"Ascii"]
-
-let ascii_path = make_path ascii_module "ascii"
-
-let ascii_kn = make_kn ascii_module "ascii"
-let path_of_Ascii = ((ascii_kn,0),1)
-let static_glob_Ascii  = ConstructRef path_of_Ascii
-
-let make_reference id = find_reference "Ascii interpretation" ascii_module id
-let glob_Ascii = lazy (make_reference "Ascii")
-
-open Lazy
-
-let interp_ascii dloc p =
-  let rec aux n p = 
-     if n = 0 then [] else
-     let mp = p mod 2 in
-     RRef (dloc,if mp = 0 then glob_false else glob_true)
-     :: (aux (n-1) (p/2)) in
-  RApp (dloc,RRef(dloc,force glob_Ascii), aux 8 p)
-
-let interp_ascii_string dloc s =
-  let p = 
-    if String.length s = 1 then int_of_char s.[0]
-    else
-      if 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 (dloc,"interp_ascii_string",
-	  str "Expects a single character or a three-digits ascii code.") in
-  interp_ascii dloc p
-
-let uninterp_ascii r =
-  let rec uninterp_bool_list n = function
-    | [] when n = 0 -> 0
-    | RRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | RRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
-    | _ -> raise Non_closed_ascii in
-  try 
-    let rec aux = function
-    | RApp (_,RRef (_,k),l) when k = 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 r = Option.map make_ascii_string (uninterp_ascii r)
-
-let _ =
-  Notation.declare_string_interpreter "char_scope"
-    (ascii_path,ascii_module)
-    interp_ascii_string
-    ([RRef (dummy_loc,static_glob_Ascii)], uninterp_ascii_string, true)