[location] Switch glob_constr to Loc.located

1 files changed, 23 insertions, 22 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 48ae93f3e..6696e174b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -324,46 +324,46 @@ 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 = function
-  | GVar (_,id) ->
+let rec pat_of_raw metas vars = Loc.with_loc (fun ~loc -> function
+  | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
-  | GPatVar (_,(false,n)) ->
+  | GPatVar (false,n) ->
       metas := n::!metas; PMeta (Some n)
-  | GRef (_,gr,_) ->
+  | GRef (gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp (_, GPatVar (_,(true,n)), cl) ->
+  | GApp ((_, GPatVar (true,n)), cl) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | GApp (_,c,cl) ->
+  | GApp (c,cl) ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
-  | GLambda (_,na,bk,c1,c2) ->
+  | GLambda (na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | GProd (_,na,bk,c1,c2) ->
+  | GProd (na,bk,c1,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | GLetIn (_,na,c1,t,c2) ->
+  | GLetIn (na,c1,t,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
-  | GSort (_,s) ->
+  | GSort s ->
       PSort s
   | GHole _ ->
       PMeta None
-  | GCast (_,c,_) ->
+  | GCast (c,_) ->
       warn_cast_in_pattern ();
       pat_of_raw metas vars c
-  | GIf (_,c,(_,None),b1,b2) ->
+  | GIf (c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
-  | GLetTuple (loc,nal,(_,None),b,c) ->
-      let mkGLambda c na =
-	GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+  | 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 c = List.fold_left mkGLambda c nal in
       let cip =
 	{ cip_style = LetStyle;
@@ -374,9 +374,9 @@ let rec pat_of_raw metas vars = function
       let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
       PCase (cip, PMeta None, pat_of_raw metas vars b,
              [0,tags,pat_of_raw metas vars c])
-  | GCases (loc,sty,p,[c,(na,indnames)],brs) ->
+  | GCases (sty,p,[c,(na,indnames)],brs) ->
       let get_ind = function
-	| (_,_,[_, PatCstr((ind,_),_,_)],_)::_ -> Some ind
+	| (_,(_,[_, PatCstr((ind,_),_,_)],_))::_ -> Some ind
 	| _ -> None
       in
       let ind_tags,ind = match indnames with
@@ -389,7 +389,7 @@ let rec pat_of_raw metas vars = 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 (_, GHole _)), _ -> PMeta None
 	| Some p, None ->
             user_err ~loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
@@ -404,7 +404,8 @@ let rec pat_of_raw metas vars = function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
-  | r -> err ~loc:(loc_of_glob_constr r) (Pp.str "Non supported pattern.")
+  | r -> err ~loc (Pp.str "Non supported pattern.")
+  )
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
@@ -415,8 +416,8 @@ and pats_of_glob_branches loc metas vars ind brs =
   in
   let rec get_pat indexes = function
     | [] -> false, []
-    | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
-    | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs ->
+    | [(_,(_,[_, PatVar(Anonymous)],(_,GHole _)))] -> true, [] (* ends with _ => _ *)
+    | (_,(_,[_, PatCstr((indsp,j),lv,_)],br)) :: brs ->
       let () = match ind with
       | Some sp when eq_ind sp indsp -> ()
       | _ ->
@@ -431,7 +432,7 @@ and pats_of_glob_branches loc metas vars ind brs =
       let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
       let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
       ext, ((j-1, tags, pat) :: pats)
-    | (loc,_,_,_) :: _ -> err ~loc (Pp.str "Non supported pattern.")
+    | (loc,(_,_,_)) :: _ -> err ~loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs