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