[location] [ast] Port module AST to CAst

1 files changed, 10 insertions, 10 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 84d846afd..1884b6927 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,7 +324,7 @@ let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
     (fun () -> Pp.strbrk "Casts are ignored in patterns")
 
-let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
+let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
   | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
@@ -333,7 +333,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
   | GRef (gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp ((_, GPatVar (true,n)), cl) ->
+  | GApp ({ CAst.v = GPatVar (true,n) }, cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
   | GApp (c,cl) ->
       PApp (pat_of_raw metas vars c,
@@ -362,8 +362,8 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda c na = Loc.tag ?loc @@
-	GLambda (na,Explicit, Loc.tag @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+      let mkGLambda c na = CAst.make ?loc @@
+	GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
       let c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;
@@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
              [0,tags,pat_of_raw metas vars c])
   | GCases (sty,p,[c,(na,indnames)],brs) ->
       let get_ind = function
-	| (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind
+	| (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind
 	| _ -> None
       in
       let ind_tags,ind = match indnames with
@@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
 	| Some p, Some (_,(_,nal)) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-        | (None | Some (_, GHole _)), _ -> PMeta None
+        | (None | Some { CAst.v = GHole _}), _ -> PMeta None
 	| Some p, None ->
             user_err ?loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
@@ -409,15 +409,15 @@ let rec pat_of_raw metas vars = Loc.with_loc (fun ?loc -> function
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
-    | _, PatVar na ->
+    | { CAst.v = PatVar na } ->
       name_iter (fun n -> metas := n::!metas) na;
       na
-    | loc, PatCstr(_,_,_) -> err ?loc (Pp.str "Non supported pattern.")
+    | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.")
   in
   let rec get_pat indexes = function
     | [] -> false, []
-    | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *)
-    | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs ->
+    | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *)
+    | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs ->
       let () = match ind with
       | Some sp when eq_ind sp indsp -> ()
       | _ ->