From 158f40db9482ead89befbf9bc9ad45ff8a60b75f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 14:23:53 +0100
Subject: [location] Switch glob_constr to Loc.located

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

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

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index de0fa77eff..539670722d 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -33,23 +33,23 @@ let glob_EmptyString = lazy (make_reference "EmptyString")
 
 open Lazy
 
-let interp_string dloc s =
+let interp_string loc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then GRef (dloc, force glob_EmptyString, None) else
-     GApp (dloc,GRef (dloc, force glob_String, None),
-       [interp_ascii dloc (int_of_char s.[n]); aux (n+1)])
+     if n = le then Loc.tag ~loc @@ GRef (force glob_EmptyString, None) else
+     Loc.tag ~loc @@ GApp (Loc.tag ~loc @@ GRef (force glob_String, None),
+       [interp_ascii loc (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
-    | GApp (_,GRef (_,k,_),[a;s]) when eq_gr k (force glob_String) ->
+    | _, GApp ((_, GRef (k,_)),[a;s]) when eq_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 eq_gr z (force glob_EmptyString) ->
+    | _, GRef (z,_) when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -61,6 +61,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([GRef (Loc.ghost,static_glob_String,None);
-      GRef (Loc.ghost,static_glob_EmptyString,None)],
+    ([Loc.tag @@ GRef (static_glob_String,None);
+      Loc.tag @@ GRef (static_glob_EmptyString,None)],
      uninterp_string, true)
-- 
cgit v1.2.3


From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 plugins/syntax/string_syntax.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

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

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 539670722d..49cb9355c8 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -33,12 +33,12 @@ let glob_EmptyString = lazy (make_reference "EmptyString")
 
 open Lazy
 
-let interp_string loc s =
+let interp_string ?loc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then Loc.tag ~loc @@ GRef (force glob_EmptyString, None) else
-     Loc.tag ~loc @@ GApp (Loc.tag ~loc @@ GRef (force glob_String, None),
-       [interp_ascii loc (int_of_char s.[n]); aux (n+1)])
+     if n = le then Loc.tag ?loc @@ GRef (force glob_EmptyString, None) else
+     Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef (force glob_String, None),
+       [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
 let uninterp_string r =
-- 
cgit v1.2.3


From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 9 Apr 2017 03:35:20 +0200
Subject: [location] [ast] Port module AST to CAst

---
 plugins/syntax/string_syntax.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

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

diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index 49cb9355c8..b7f13b0400 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -36,8 +36,8 @@ open Lazy
 let interp_string ?loc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then Loc.tag ?loc @@ GRef (force glob_EmptyString, None) else
-     Loc.tag ?loc @@ GApp (Loc.tag ?loc @@ GRef (force glob_String, None),
+     if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else
+     CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None),
        [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
@@ -45,11 +45,11 @@ let uninterp_string r =
   try
     let b = Buffer.create 16 in
     let rec aux = function
-    | _, GApp ((_, GRef (k,_)),[a;s]) when eq_gr k (force glob_String) ->
+    | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_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 eq_gr z (force glob_EmptyString) ->
+    | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -61,6 +61,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([Loc.tag @@ GRef (static_glob_String,None);
-      Loc.tag @@ GRef (static_glob_EmptyString,None)],
+    ([CAst.make @@ GRef (static_glob_String,None);
+      CAst.make @@ GRef (static_glob_EmptyString,None)],
      uninterp_string, true)
-- 
cgit v1.2.3