From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 plugins/syntax/string_syntax.ml | 16 +++++++---------
 1 file changed, 7 insertions(+), 9 deletions(-)

(limited to 'plugins/syntax/string_syntax.ml')

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 534605c8..d670f602 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(*i $Id: string_syntax.ml 12337 2009-09-17 15:58:14Z glondu $ i*)
-
 open Pp
 open Util
 open Names
@@ -15,7 +13,7 @@ open Pcoq
 open Libnames
 open Topconstr
 open Ascii_syntax
-open Rawterm
+open Glob_term
 open Coqlib
 
 exception Non_closed_string
@@ -39,8 +37,8 @@ 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),
+     if n = le then GRef (dloc, force glob_EmptyString) else
+     GApp (dloc,GRef (dloc, force glob_String),
        [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -48,11 +46,11 @@ 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 ->
+    | GApp (_,GRef (_,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 ->
+    | GRef (_,z) when z = force glob_EmptyString ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -64,6 +62,6 @@ 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)],
+    ([GRef (dummy_loc,static_glob_String);
+      GRef (dummy_loc,static_glob_EmptyString)],
      uninterp_string, true)
-- 
cgit v1.2.3