[location] [ast] Port module AST to CAst

1 files changed, 17 insertions, 16 deletions

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index c11c9f83b..9a0dfbf1c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -158,10 +158,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((Loc.tag ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
-let mkRHole = Loc.tag @@ GHole (InternalHole, IntroAnonymous, None)
-let mkRApp f args = if args = [] then f else Loc.tag @@ GApp (f, args)
-let mkRCast rc rt =  Loc.tag @@ GCast (rc, dC rt)
-let mkRLambda n s t = Loc.tag @@ GLambda (n, Explicit, s, t)
+let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None)
+let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
+let mkRCast rc rt =  CAst.make @@ GCast (rc, dC rt)
+let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
 
 (* ssrterm conbinators *)
 let combineCG t1 t2 f g = match t1, t2 with
@@ -1022,7 +1022,7 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern
 let id_of_cpattern = let open CAst in function
   | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x
   | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x
-  | _,((_, GRef (VarRef x, _)) ,None) -> Some x
+  | _,({ v = GRef (VarRef x, _)} ,None) -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
@@ -1121,9 +1121,10 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   let eAsXInT e x t = E_As_X_In_T(e,x,t) in
   let mkG ?(k=' ') x = k,(x,None) in
   let decode ist t ?reccall f g =
+    let open CAst in
     try match (pf_intern_term ist gl t) with
-    | _, GCast((_, GHole _),CastConv((_, GLambda(Name x,_,_,c)))) -> f x (' ',(c,None))
-    | _, GVar id
+    | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None))
+    | { v = GVar id }
       when Id.Map.mem id ist.lfun &&
            not(Option.is_empty reccall) &&
            not(Option.is_empty wit_ssrpatternarg) ->
@@ -1164,18 +1165,18 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         thin name sigma e)
       sigma new_evars in
     sigma in
-  let red = let rec decode_red (ist,red) = match red with
-    | T(k,((_, GCast ((_, GHole _),CastConv((_, GLambda (Name id,_,_,t))))),None))
+  let red = let rec decode_red (ist,red) = let open CAst in match red with
+    | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None))
         when let id = string_of_id id in let len = String.length id in
         (len > 8 && String.sub id 0 8 = "_ssrpat_") ->
         let id = string_of_id id in let len = String.length id in
         (match String.sub id 8 (len - 8), t with
-        | "In", (_, GApp( _, [t])) -> decodeG t xInT (fun x -> T x)
-        | "In", (_, GApp( _, [e; t])) -> decodeG t (eInXInT (mkG e)) (bad_enc id)
-        | "In", (_, GApp( _, [e; t; e_in_t])) ->
+        | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x)
+        | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id)
+        | "In", { v = GApp( _, [e; t; e_in_t]) } ->
             decodeG t (eInXInT (mkG e))
               (fun _ -> decodeG e_in_t xInT (fun _ -> assert false))
-        | "As", (_, GApp(_, [e; t])) -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
+        | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
         | _ -> bad_enc id ())
     | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x)
     | In_T t -> decode ist t inXInT inT
@@ -1201,7 +1202,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn ?loc x (a,(g,c)) = match c with
   | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ?loc) b))
-  | None -> a,(Loc.tag ?loc @@ GLetIn (x, Loc.tag ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
+  | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
   match red with
   | T t -> let sigma, t = interp_term ist gl t in sigma, T t
   | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
@@ -1374,10 +1375,10 @@ let pf_fill_occ_term gl occ t =
   let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
   cl, t
 
-let cpattern_of_id id = ' ', (Loc.tag @@ GRef (VarRef  id, None), None)
+let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef  id, None), None)
 
 let is_wildcard : cpattern -> bool = function
-  | _,(_,Some { CAst.v = CHole _ } | (_, GHole _),None) -> true
+  | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true
   | _ -> false
 
 (* "ssrpattern" *)