[location] Move Glob_term.cases_pattern to located.

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

4 files changed, 65 insertions, 62 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 255de8500d..b3059f5d04 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -182,7 +182,7 @@ let add_patt_for_params ind l =
 
 let add_cpatt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn  (Inductiveops.inductive_nparamdecls ind) (PatVar (Loc.ghost,Anonymous)) l
+    Util.List.addn  (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ PatVar Anonymous) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -291,7 +291,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
   match pat with
-    | PatCstr(loc,cstrsp,args,na)
+    | loc, PatCstr(cstrsp,args,na)
 	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
       let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
@@ -312,9 +312,9 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
       match pat with
-	| PatVar (loc,Name id)   -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
-	| PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None
-	| PatCstr(loc,cstrsp,args,na) ->
+	| loc, PatVar (Name id)   -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
+	| loc, PatVar (Anonymous) -> Loc.tag ~loc @@ CPatAtom None
+	| loc, PatCstr(cstrsp,args,na) ->
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
 	  let p =
 	    try
@@ -391,20 +391,20 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
       in
       assert (List.is_empty substlist);
       mkPat loc qid (List.rev_append l1 l2')
-and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
+and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
     try
       if List.mem keyrule !print_non_active_notations then raise No_match;
       match t with
-	| PatCstr (loc,cstr,_,na) ->
+	| PatCstr (cstr,_,na) ->
 	  let p = apply_notation_to_pattern loc (ConstructRef cstr)
-	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
+	    (match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in
 	  insert_pat_alias loc p na
-	| PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None
-	| PatVar (loc,Name id)   -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
+	| PatVar Anonymous -> Loc.tag ~loc @@ CPatAtom None
+	| PatVar (Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
     with
-	No_match -> extern_notation_pattern allscopes vars t rules
+	No_match -> extern_notation_pattern allscopes vars (loc, t) rules
 
 let rec extern_notation_ind_pattern allscopes vars ind args = function
   | [] -> raise No_match
@@ -750,7 +750,7 @@ let rec extern inctx scopes vars r =
                  (sub_extern false scopes vars tm,
                   na',
                   Option.map (fun (loc,ind,nal) ->
-                              let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
+                              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
                              ) x))
@@ -1008,7 +1008,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
 
 let any_any_branch =
   (* | _ => _ *)
-  (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+  (loc,[],[Loc.tag ~loc @@ PatVar Anonymous],GHole (loc,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
 
 let rec glob_of_pat env sigma = function
   | PRef ref -> GRef (loc,ref,None)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4af89e1ef7..4960d7332e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -591,14 +591,14 @@ let rec subordinate_letins letins = function
       letins,[]
 
 let terms_of_binders bl =
-  let rec term_of_pat = function
-    | PatVar (loc,Name id)   -> Loc.tag ~loc @@ CRef (Ident (loc,id), None)
-    | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
-    | PatCstr (loc,c,l,_) ->
+  let rec term_of_pat pt = Loc.map_with_loc (fun ~loc -> function
+    | PatVar (Name id)   -> CRef (Ident (loc,id), None)
+    | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
+    | PatCstr (c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
        let hole = Loc.tag ~loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
-       Loc.tag ~loc @@ CAppExpl ((None,r,None),params @ List.map term_of_pat l) in
+       CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
     | GLocalAssum (loc,Name id,_,_)::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
@@ -1015,8 +1015,8 @@ let chop_params_pattern loc ind args with_letin =
     else Inductiveops.inductive_nparams ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
-  List.iter (function PatVar(_,Anonymous) -> ()
-    | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
+  List.iter (function _, PatVar Anonymous -> ()
+    | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
   args
 
 let find_constructor loc add_params ref =
@@ -1036,7 +1036,7 @@ let find_constructor loc add_params ref =
           then Inductiveops.inductive_nparamdecls ind
           else Inductiveops.inductive_nparams ind
       in
-      List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
+      List.make nb ([], [(Id.Map.empty, Loc.tag @@ PatVar Anonymous)])
     | None -> []
 
 let find_pattern_variable = function
@@ -1358,7 +1358,7 @@ let rec intern_pat genv aliases pat =
     let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
     let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
-      (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+      (asubst, Loc.tag ~loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
   match pat with
     | loc, RCPatAlias (p, id) ->
@@ -1378,10 +1378,10 @@ let rec intern_pat genv aliases pat =
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
     | loc, RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
-      (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)])
+      (aliases.alias_ids,[aliases.alias_map, Loc.tag ~loc @@ PatVar (alias_of aliases)])
     | loc, RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
-      (ids, [asubst, PatVar (loc, alias_of aliases)])
+      (ids, [asubst, Loc.tag ~loc @@ PatVar (alias_of aliases)])
     | loc, RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
@@ -1678,14 +1678,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         let stripped_match_from_in =
           let rec aux = function
 	    | [] -> []
-	    | (_,PatVar _) :: q -> aux q
+	    | (_, (_loc, PatVar _)) :: q -> aux q
 	    | l -> l
 	  in aux match_from_in in
         let rtnpo = match stripped_match_from_in with
 	  | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
 	  | l ->
              (* Build a return predicate by expansion of the patterns of the "in" clause *)
-             let thevars,thepats = List.split l in
+             let thevars, thepats = List.split l in
              let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
              let sub_tms = List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars (* "match v1,..,vn" *) in
              let main_sub_eqn =
@@ -1695,7 +1695,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
-                 [Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
+                 [Loc.ghost,[],List.make (List.length thepats) (Loc.tag @@ PatVar Anonymous), (* "|_,..,_" *)
 		  GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)]   (* "=> _" *) in
              Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
@@ -1817,14 +1817,14 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	  let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
 	    let add_name l = function
 	      | _,Anonymous -> l
-	      | loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in
+	      | loc,(Name y as x) -> (y, Loc.tag ~loc @@ PatVar x) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
 		canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
 	      | [],[] ->
 		(add_name match_acc na, var_acc)
-	      | _::t,PatVar (loc,x)::tt ->
+	      | _::t, (loc, PatVar x)::tt ->
 		canonize_args t tt forbidden_names
 		  (add_name match_acc (loc,x)) ((loc,x)::var_acc)
 	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 04711808b7..aef0892996 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -273,7 +273,7 @@ let glob_constr_keys = function
   | _ -> [Oth]
 
 let cases_pattern_key = function
-  | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
+  | _, PatCstr (ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8b4fadb5a0..29f42d0e9e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -117,13 +117,14 @@ let name_to_ident = function
 
 let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
-let rec cases_pattern_fold_map loc g e = function
-  | PatVar (_,na) ->
-      let e',na' = g e na in e', PatVar (loc,na')
-  | PatCstr (_,cstr,patl,na) ->
+let rec cases_pattern_fold_map loc g e = Loc.with_unloc (function
+  | PatVar na ->
+      let e',na' = g e na in e', Loc.tag ~loc @@ PatVar na'
+  | PatCstr (cstr,patl,na) ->
       let e',na' = g e na in
       let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
-      e', PatCstr (loc,cstr,patl',na')
+      e', Loc.tag ~loc @@ PatCstr (cstr,patl',na')
+  )
 
 let subst_binder_type_vars l = function
   | Evar_kinds.BinderType (Name id) ->
@@ -450,14 +451,15 @@ let notation_constr_of_constr avoiding t =
   } in
   notation_constr_of_glob_constr nenv t
 
-let rec subst_pat subst pat =
+let rec subst_pat subst (loc, pat) =
   match pat with
-  | PatVar _ -> pat
-  | PatCstr (loc,((kn,i),j),cpl,n) ->
+  | PatVar _ -> (loc, pat)
+  | PatCstr (((kn,i),j),cpl,n) ->
       let kn' = subst_mind subst kn
       and cpl' = List.smartmap (subst_pat subst) cpl in
+      Loc.tag ~loc @@
         if kn' == kn && cpl' == cpl then pat else
-          PatCstr (loc,((kn',i),j),cpl',n)
+          PatCstr (((kn',i),j),cpl',n)
 
 let rec subst_notation_constr subst bound raw =
   match raw with
@@ -662,11 +664,11 @@ let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
   (terms,onlybinders,termlists,(x,bl)::binderlists)
 
 let rec pat_binder_of_term = function
-  | GVar (loc, id) -> PatVar (loc, Name id)
+  | GVar (loc, id) -> Loc.tag ~loc @@ PatVar (Name id)
   | GApp (loc, GRef (_,ConstructRef cstr,_), l) ->
      let nparams = Inductiveops.inductive_nparams (fst cstr) in
      let _,l = List.chop nparams l in
-     PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous)
+     Loc.tag ~loc @@ PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
   | _ -> raise No_match
 
 let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
@@ -738,16 +740,17 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var
         else (fst alp,(id1,id2)::snd alp),sigma
   with Not_found -> alp, add_binding_env alp sigma var v
 
-let rec map_cases_pattern_name_left f = function
-  | PatVar (loc,na) -> PatVar (loc,f na)
-  | PatCstr (loc,c,l,na) -> PatCstr (loc,c,List.map_left (map_cases_pattern_name_left f) l,f na)
+let rec map_cases_pattern_name_left f = Loc.map (function
+  | PatVar na -> PatVar (f na)
+  | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
+  )
 
 let rec fold_cases_pattern_eq f x p p' = match p, p' with
-  | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na)
-  | PatCstr (loc,c,l,na), PatCstr (_,c',l',na') when eq_constructor c c' ->
+  | (loc, PatVar na), (_, PatVar na') -> let x,na = f x na na' in x, Loc.tag ~loc @@ PatVar na
+  | (loc, PatCstr (c,l,na)), (_, PatCstr (c',l',na')) when eq_constructor c c' ->
      let x,l = fold_cases_pattern_list_eq f x l l' in
      let x,na = f x na na' in
-     x, PatCstr (loc,c,l,na)
+     x, Loc.tag ~loc @@ PatCstr (c,l,na)
   | _ -> failwith "Not equal"
 
 and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
@@ -758,9 +761,9 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
      x, p :: pl
   | _ -> assert false
 
-let rec cases_pattern_eq p1 p2 = match p1, p2 with
-| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
-| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
+let rec cases_pattern_eq (_,p1) (_,p2) = match p1, p2 with
+| PatVar na1, PatVar na2 -> Name.equal na1 na2
+| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
   eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
   Name.equal na1 na2
 | _ -> false
@@ -878,10 +881,10 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
 
-let rec match_cases_pattern_binders metas acc pat1 pat2 =
-  match (pat1,pat2) with
-  | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2
-  | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2)
+let rec match_cases_pattern_binders metas acc (_, pat1) (_, pat2) =
+  match pat1, pat2 with
+  | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
+  | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
       List.fold_left2 (match_cases_pattern_binders metas)
 	(match_names metas acc na1 na2) patl1 patl2
@@ -1173,7 +1176,7 @@ let match_notation_constr u c (metas,pat) =
 let add_patterns_for_params ind l =
   let mib,_ = Global.lookup_inductive ind in
   let nparams = mib.Declarations.mind_nparams in
-    Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
+    Util.List.addn nparams (Loc.tag @@ PatVar Anonymous) l
 
 let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
   try
@@ -1197,13 +1200,13 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
   let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in
   (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
 
-let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
- match (a1,a2) with
-  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
-  | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
-  | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
+let rec match_cases_pattern metas (terms,(),termlists,() as sigma) (loc, a1) a2 =
+ match a1, a2 with
+  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 (loc, r1)),(0,[])
+  | PatVar Anonymous, NHole _ -> sigma,(0,[])
+  | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
       sigma,(0,add_patterns_for_params (fst r1) largs)
-  | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
+  | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = add_patterns_for_params (fst r1) args1 in
       let le2 = List.length l2 in
@@ -1215,7 +1218,7 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
   | r1, NList (x,y,iter,termin,lassoc) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-	metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[])
+	metas (terms,(),termlists,()) (loc, r1) x y iter termin lassoc),(0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =