From ad3aab9415b98a247a6cbce05752632c3c42391c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 16 Jan 2017 13:02:55 +0100
Subject: [location] Move Glob_term.cases_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.
---
 pretyping/patternops.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping/patternops.ml')

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b16d044956..8c570dffee 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -376,7 +376,7 @@ let rec pat_of_raw metas vars = function
              [0,tags,pat_of_raw metas vars c])
   | GCases (loc,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
@@ -408,15 +408,15 @@ let rec pat_of_raw metas vars = function
 
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
-    | PatVar(_,na) ->
+    | _, PatVar na ->
       name_iter (fun n -> metas := n::!metas) na;
       na
-    | PatCstr(loc,_,_,_) -> err ~loc (Pp.str "Non supported pattern.")
+    | loc, PatCstr(_,_,_) -> 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 ->
+    | [(_,_,[_, PatVar(Anonymous)],GHole _)] -> true, [] (* ends with _ => _ *)
+    | (_,_,[_, PatCstr((indsp,j),lv,_)],br) :: brs ->
       let () = match ind with
       | Some sp when eq_ind sp indsp -> ()
       | _ ->
-- 
cgit v1.2.3