[location] Move Glob_term.predicate_pattern to located.

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

8 files changed, 22 insertions, 22 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b3059f5d0..d45f3a9f1 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -749,7 +749,7 @@ let rec extern inctx scopes vars r =
                    | Name _, _ -> Some (Loc.ghost,na) in
                  (sub_extern false scopes vars tm,
                   na',
-                  Option.map (fun (loc,ind,nal) ->
+                  Option.map (fun (loc,(ind,nal)) ->
                               let args = List.map (fun x -> Loc.tag @@ PatVar x) nal in
                               let fullargs = add_cpatt_for_params ind args in
                               extern_ind_pattern_in_scope scopes vars ind fullargs
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4960d7332..f814205dc 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1836,7 +1836,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
 	  canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
-	match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
+	match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
     | None ->
       [], None in
     (tm',(snd na,typ)), extra_id, match_td
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 29f42d0e9..a25fd81f3 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -179,7 +179,7 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
 	| Some (ind,nal) ->
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
 	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
-	  e',Some (loc,ind,nal') in
+	  e',Some (loc,(ind,nal')) in
 	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
@@ -356,8 +356,8 @@ let notation_constr_and_vars_of_glob_constr a =
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  Option.iter
-	    (fun (_,_,nl) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+	    (fun (_,(_,nl)) -> List.iter (add_name found) nl) x;
+          (aux tm,(na,Option.map (fun (_,(ind,nal)) -> (ind,nal)) x))) tml,
         List.map f eqnl)
   | GLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
@@ -589,7 +589,7 @@ let abstract_return_type_context pi mklam tml rtno =
     rtno
 
 let abstract_return_type_context_glob_constr =
-  abstract_return_type_context (fun (_,_,nal) -> nal)
+  abstract_return_type_context (fun (_,(_,nal)) -> nal)
     (fun na c ->
       GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
 
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 5e771245c..7a43c44f9 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -67,7 +67,7 @@ and fix_kind =
   | GCoFix of int
 
 and predicate_pattern =
-    Name.t * (Loc.t * inductive * Name.t list) option
+    Name.t * (inductive * Name.t list) Loc.located option
       (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
 
 and tomatch_tuple = (glob_constr * predicate_pattern)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ce4610e3b..531485935 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 eef6d34ac..f3018ac64 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 27ceabf4e..4cccaaf8f 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 8c570dffe..48ae93f3e 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