[location] Move Glob_term.predicate_pattern to located.

We continue the uniformization pass. No big news here, trying to be
minimally invasive.

4 files changed, 15 insertions, 15 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ce4610e3b5..5314859358 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -342,7 +342,7 @@ let unify_tomatch_with_patterns evdref env loc typ pats realnames =
 
 let find_tomatch_tycon evdref env loc = function
   (* Try if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,realnal) ->
+  | Some (_,(ind,realnal)) ->
       mk_tycon (inductive_template evdref env loc ind),Some (List.rev realnal)
   | None ->
       empty_tycon,None
@@ -360,7 +360,7 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) =
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
   (j.uj_val,t)
 
-let coerce_to_indtype typing_fun evdref env matx tomatchl =
+let coerce_to_indtype typing_fun evdref env matx tomatchl = 
   let pats = List.map (fun r ->  r.patterns) matx in
   let matx' = match matrix_transpose pats with
     | [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
@@ -1852,7 +1852,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	    | None -> (match bo with
 		       | None -> [LocalAssum (na, lift n typ)]
 		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
-	    | Some (loc,_,_) ->
+	    | Some (loc,_) ->
  	    user_err ~loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
@@ -1863,7 +1863,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	  let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',realnal) ->
+	      | Some (loc,(ind',realnal)) ->
 		  if not (eq_ind ind ind') then
 		    user_err ~loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index eef6d34acb..f3018ac64b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -380,7 +380,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
 	      if List.for_all (Name.equal Anonymous) nl then None
-	      else Some (dl,indsp,nl) in
+	      else Some (dl,(indsp,nl)) in
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
@@ -844,9 +844,9 @@ let rec subst_glob_constr subst raw =
         let a' = subst_glob_constr subst a in
         let (n,topt) = x in
         let topt' = Option.smartmap
-          (fun (loc,(sp,i),y as t) ->
+          (fun ((loc,((sp,i),y) as t)) ->
             let sp' = subst_mind subst sp in
-            if sp == sp' then t else (loc,(sp',i),y)) topt in
+            if sp == sp' then t else (loc,((sp',i),y))) topt in
         if a == a' && topt == topt' then y else (a',(n,topt'))) rl
       and branches' = List.smartmap
 			(fun (loc,idl,cpl,r as branch) ->
@@ -919,4 +919,4 @@ let simple_cases_matrix_of_branches ind brs =
 
 let return_type_of_predicate ind nrealargs_tags pred =
   let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in
-  (List.hd nal, Some (Loc.ghost, ind, List.tl nal)), Some p
+  (List.hd nal, Some (Loc.tag (ind, List.tl nal))), Some p
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 27ceabf4e4..4cccaaf8ff 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -20,7 +20,7 @@ let cases_pattern_loc (loc, _) = loc
 let cases_predicate_names tml =
   List.flatten (List.map (function
     | (tm,(na,None)) -> [na]
-    | (tm,(na,Some (_,_,nal))) -> na::nal) tml)
+    | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml)
 
 let mkGApp loc p t =
   match p with
@@ -103,7 +103,7 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
 | _ -> false
 
 and tomatch_tuple_eq (c1, p1) (c2, p2) =
-  let eqp (_, i1, na1) (_, i2, na2) =
+  let eqp (_, (i1, na1)) (_, (i2, na2)) =
     eq_ind i1 i2 && List.equal Name.equal na1 na2
   in
   let eq_pred (n1, o1) (n2, o2) = Name.equal n1 n2 && Option.equal eqp o1 o2 in
@@ -411,10 +411,10 @@ let bound_glob_vars =
    probably be no significant penalty in doing reallocation as
    pattern-matching expressions are usually rather small. *)
 
-let map_inpattern_binders f ((loc,id,nal) as x) =
+let map_inpattern_binders f ((loc,(id,nal)) as x) =
   let r = CList.smartmap f nal in
   if r == nal then x
-  else loc,id,r
+  else loc,(id,r)
 
 let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple =
   let r = Option.smartmap (fun p -> map_inpattern_binders f p) inp in
@@ -525,7 +525,7 @@ let rec rename_glob_vars l = function
   (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
   | GCases (loc,ci,po,tomatchl,cls) ->
       let test_pred_pat (na,ino) =
-        test_na l na; Option.iter (fun (_,_,nal) -> List.iter (test_na l) nal) ino in
+        test_na l na; Option.iter (fun (_,(_,nal)) -> List.iter (test_na l) nal) ino in
       let test_clause idl = List.iter (test_id l) idl in
       let po = Option.map (rename_glob_vars l) po in
       let tomatchl = Util.List.map_left (fun (tm,x) -> test_pred_pat x; (rename_glob_vars l tm,x)) tomatchl in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 8c570dffee..48ae93f3ef 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -380,13 +380,13 @@ let rec pat_of_raw metas vars = function
 	| _ -> None
       in
       let ind_tags,ind = match indnames with
-	| Some (_,ind,nal) -> Some (List.length nal), Some ind
+	| Some (_,(ind,nal)) -> Some (List.length nal), Some ind
 	| None -> None, get_ind brs
       in
       let ext,brs = pats_of_glob_branches loc metas vars ind brs
       in
       let pred = match p,indnames with
-	| Some p, Some (_,_,nal) ->
+	| 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