[location] Move Glob_term.cases_pattern to located.

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

15 files changed, 188 insertions, 178 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 255de8500..b3059f5d0 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 4af89e1ef..4960d7332 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 04711808b..aef089299 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 8b4fadb5a..29f42d0e9 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 =
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index ced5a8b44..5e771245c 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -24,10 +24,11 @@ type existential_name = Id.t
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)
-type cases_pattern =
-  | PatVar of Loc.t * Name.t
-  | PatCstr of Loc.t * constructor * cases_pattern list * Name.t
+type cases_pattern_r =
+  | PatVar  of Name.t
+  | PatCstr of constructor * cases_pattern list * Name.t
       (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *)
+and cases_pattern = cases_pattern_r Loc.located
 
 (** Representation of an internalized (or in other words globalized) term. *)
 type glob_constr =
diff --git a/lib/loc.ml b/lib/loc.ml
index 8ae8fe25d..8d7432ff4 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -63,7 +63,8 @@ type 'a located = t * 'a
 let to_pair x = x
 let tag ?loc x = Option.default ghost loc, x
 
-let with_loc f (loc, x) = f ~loc x
+let with_loc   f (loc, x) = f ~loc x
+let with_unloc f (_,x) = f x
 
 let map f (l,x) = (l, f x)
 let map_with_loc f (loc, x) = (loc, f ~loc x)
diff --git a/lib/loc.mli b/lib/loc.mli
index 7fc8efaa8..3f484bc4c 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -62,6 +62,7 @@ val to_pair : 'a located -> t * 'a
 val tag : ?loc:t -> 'a -> 'a located
 
 val with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b
+val with_unloc : ('a -> 'b) -> 'a located -> 'b
 
 val map : ('a -> 'b) -> 'a located -> 'b located
 val map_with_loc : (loc:t -> 'a -> 'b) -> 'a located -> 'b located
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4b942c989..85d465a4b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -345,12 +345,12 @@ let raw_push_named (na,raw_value,raw_typ) env =
 
 
 let add_pat_variables pat typ env : Environ.env =
-  let rec add_pat_variables env pat typ  : Environ.env =
+  let rec add_pat_variables env (loc, pat) typ  : Environ.env =
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
     match pat with
-      | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
-      | PatCstr(_,c,patl,na) ->
+      | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
+      | PatCstr(c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
 	    try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
 	    with Not_found -> assert false
@@ -398,11 +398,11 @@ let add_pat_variables pat typ env : Environ.env =
 
 
 
-let rec pattern_to_term_and_type env typ  = function
-  | PatVar(loc,Anonymous) -> assert false
-  | PatVar(loc,Name id) ->
+let rec pattern_to_term_and_type env typ  = Loc.with_unloc (function
+  | PatVar Anonymous -> assert false
+  | PatVar (Name id) ->
 	mkGVar id
-  | PatCstr(loc,constr,patternl,_) ->
+  | PatCstr(constr,patternl,_) ->
       let cst_narg =
 	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
@@ -430,6 +430,7 @@ let rec pattern_to_term_and_type env typ  = function
       mkGApp(mkGRef(ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
+  )
 
 (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
    of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 99f50437b..51ca8c471 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -194,19 +194,19 @@ let change_vars =
 
 
 
-let rec alpha_pat excluded pat =
+let rec alpha_pat excluded (loc, pat) =
   match pat with
-    | PatVar(loc,Anonymous) ->
+    | PatVar Anonymous ->
 	let new_id = Indfun_common.fresh_id excluded "_x" in
-	PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty
-    | PatVar(loc,Name id) ->
+	(Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+    | PatVar(Name id) ->
 	if Id.List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
-	  PatVar(loc,Name new_id),(new_id::excluded),
+	  (Loc.tag ~loc @@ PatVar(Name new_id)),(new_id::excluded),
 	(Id.Map.add id new_id Id.Map.empty)
-	else pat,excluded,Id.Map.empty
-    | PatCstr(loc,constr,patl,na) ->
+	else (Loc.tag ~loc pat),excluded,Id.Map.empty
+    | PatCstr(constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when Id.List.mem id excluded ->
@@ -223,7 +223,7 @@ let rec alpha_pat excluded pat =
 	    ([],new_excluded,map)
 	    patl
 	in
-	PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map
+        (Loc.tag ~loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
 
 let alpha_patl excluded patl  =
   let patl,new_excluded,map =
@@ -241,12 +241,12 @@ let alpha_patl excluded patl  =
 
 
 let raw_get_pattern_id pat acc =
-  let rec get_pattern_id pat =
+  let rec get_pattern_id (loc, pat) =
     match pat with
-      | PatVar(loc,Anonymous) -> assert false
-      | PatVar(loc,Name id) ->
+      | PatVar(Anonymous) -> assert false
+      | PatVar(Name id) ->
 	  [id]
-      | PatCstr(loc,constr,patternl,_) ->
+      | PatCstr(constr,patternl,_) ->
 	  List.fold_right
 	  (fun pat idl ->
 	     let idl' = get_pattern_id pat in
@@ -425,11 +425,11 @@ let is_free_in id =
 
 
 
-let rec pattern_to_term  = function
-  | PatVar(loc,Anonymous) -> assert false
-  | PatVar(loc,Name id) ->
+let rec pattern_to_term pt = Loc.with_unloc (function
+  | PatVar Anonymous -> assert false
+  | PatVar(Name id) ->
 	mkGVar id
-  | PatCstr(loc,constr,patternl,_) ->
+  | PatCstr(constr,patternl,_) ->
       let cst_narg =
 	Inductiveops.constructor_nallargs_env
 	  (Global.env ())
@@ -448,7 +448,7 @@ let rec pattern_to_term  = function
       mkGApp(mkGRef(Globnames.ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
-
+  ) pt
 
 
 let replace_var_by_term x_id term =
@@ -533,8 +533,8 @@ let rec are_unifiable_aux  = function
   | [] -> ()
   | eq::eqs ->
       match eq with
-	 | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs
-	 | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
+	 | (_,PatVar _),_ | _,(_,PatVar _) -> are_unifiable_aux eqs
+	 | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) ->
 	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
@@ -555,8 +555,8 @@ let rec eq_cases_pattern_aux  = function
   | [] -> ()
   | eq::eqs ->
       match eq with
-	 | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs
-	 | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
+	 | (_,PatVar _),(_,PatVar _) -> eq_cases_pattern_aux eqs
+	 | (_,PatCstr(constructor1,cpl1,_)),(_,PatCstr(constructor2,cpl2,_)) ->
 	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
@@ -576,10 +576,11 @@ let eq_cases_pattern pat1 pat2 =
 
 
 let ids_of_pat =
-  let rec ids_of_pat ids = function
-    | PatVar(_,Anonymous) -> ids
-    | PatVar(_,Name id) -> Id.Set.add id ids
-    | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl
+  let rec ids_of_pat ids = Loc.with_unloc (function
+    | PatVar Anonymous -> ids
+    | PatVar(Name id) -> Id.Set.add id ids
+    | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl
+    )
   in
   ids_of_pat Id.Set.empty
 
@@ -679,12 +680,12 @@ let zeta_normalize =
 
 let expand_as =
 
-  let rec add_as map pat =
+  let rec add_as map (loc, pat) =
     match pat with
       | PatVar _ -> map
-      | PatCstr(_,_,patl,Name id) ->
-	  Id.Map.add id (pattern_to_term pat) (List.fold_left add_as map patl)
-      | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
+      | PatCstr(_,patl,Name id) ->
+	  Id.Map.add id (pattern_to_term (loc, pat)) (List.fold_left add_as map patl)
+      | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map rt =
     match rt with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1e405d2c9..ee7b33227 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -193,10 +193,10 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
 	(d0,RegularStyle,None,
 	 [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
 	  (Anonymous,None)],
-	 [d0, [v_id], [PatCstr(d0,(destIndRef
+	 [d0, [v_id], [d0,PatCstr((destIndRef
 				     (delayed_force coq_sig_ref),1),
-			       [PatVar(d0, Name v_id);
-				PatVar(d0, Anonymous)],
+			       [d0, PatVar(Name v_id);
+				d0, PatVar(Anonymous)],
 			       Anonymous)],
 	  GVar(d0,v_id)])
     in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6bc2a4f94..ce4610e3b 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -95,7 +95,7 @@ let msg_may_need_inversion () =
 
 (* Utils *)
 let make_anonymous_patvars n =
-  List.make n (PatVar (Loc.ghost,Anonymous))
+  List.make n (Loc.tag @@ PatVar Anonymous)
 
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
@@ -178,7 +178,7 @@ and build_glob_pattern args = function
   | Top -> args
   | MakeConstructor (pci, rh) ->
       glob_pattern_of_partial_history
-	[PatCstr (Loc.ghost, pci, args, Anonymous)] rh
+	[Loc.tag @@ PatCstr (pci, args, Anonymous)] rh
 
 let complete_history = glob_pattern_of_partial_history []
 
@@ -188,12 +188,12 @@ let pop_history_pattern = function
   | Continuation (0, l, Top) ->
       Result (List.rev l)
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
-      feed_history (PatCstr (Loc.ghost,pci,List.rev l,Anonymous)) rh
+      feed_history (Loc.tag @@ PatCstr (pci,List.rev l,Anonymous)) rh
   | _ ->
       anomaly (Pp.str "Constructor not yet filled with its arguments")
 
 let pop_history h =
-  feed_history (PatVar (Loc.ghost, Anonymous)) h
+  feed_history (Loc.tag @@ PatVar Anonymous) h
 
 (* Builds a continuation expecting [n] arguments and building [ci] applied
    to this [n] arguments *)
@@ -273,8 +273,8 @@ type 'a pattern_matching_problem =
 
 let rec find_row_ind = function
     [] -> None
-  | PatVar _ :: l -> find_row_ind l
-  | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
+  | (_, PatVar _) :: l -> find_row_ind l
+  | (loc, PatCstr(c,_,_)) :: _ -> Some (loc,c)
 
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
@@ -427,9 +427,10 @@ let current_pattern eqn =
     | pat::_ -> pat
     | [] -> anomaly (Pp.str "Empty list of patterns")
 
-let alias_of_pat = function
-  | PatVar (_,name) -> name
-  | PatCstr(_,_,_,name) -> name
+let alias_of_pat = Loc.with_loc (fun ~loc -> function
+  | PatVar name -> name
+  | PatCstr(_,_,name) -> name
+  )
 
 let remove_current_pattern eqn =
   match eqn.patterns with
@@ -472,13 +473,13 @@ let rec adjust_local_defs loc = function
   | (pat :: pats, LocalAssum _ :: decls) ->
       pat :: adjust_local_defs loc (pats,decls)
   | (pats, LocalDef _ :: decls) ->
-      PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls)
+      (Loc.tag ~loc @@ PatVar Anonymous) :: adjust_local_defs loc (pats,decls)
   | [], [] -> []
   | _ -> raise NotAdjustable
 
 let check_and_adjust_constructor env ind cstrs = function
-  | PatVar _ as pat -> pat
-  | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
+  | _,   PatVar _ as pat -> pat
+  | loc, PatCstr (((_,i) as cstr),args,alias) as pat ->
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
       if eq_ind ind' ind then
@@ -489,7 +490,7 @@ let check_and_adjust_constructor env ind cstrs = function
 	else
 	  try
 	    let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
-	    in PatCstr (loc, cstr, args', alias)
+	    in Loc.tag ~loc @@ PatCstr (cstr, args', alias)
 	  with NotAdjustable ->
 	    error_wrong_numarg_constructor ~loc env cstr nb_args_constr
       else
@@ -502,8 +503,8 @@ let check_and_adjust_constructor env ind cstrs = function
 let check_all_variables env sigma typ mat =
   List.iter
     (fun eqn -> match current_pattern eqn with
-       | PatVar (_,id) -> ()
-       | PatCstr (loc,cstr_sp,_,_) ->
+       | _,   PatVar id -> ()
+       | loc, PatCstr (cstr_sp,_,_) ->
 	   error_bad_pattern ~loc env sigma cstr_sp typ)
     mat
 
@@ -529,8 +530,8 @@ let occur_in_rhs na rhs =
     | Name id -> Id.List.mem id rhs.rhs_vars
 
 let is_dep_patt_in eqn = function
-  | PatVar (_,name) -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
-  | PatCstr _ -> true
+  | _, PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
+  | _, PatCstr _ -> true
 
 let mk_dep_patt_row (pats,_,eqn) =
   List.map (is_dep_patt_in eqn) pats
@@ -750,7 +751,7 @@ let recover_and_adjust_alias_names names sign =
   | x::names, LocalAssum (_,t)::sign ->
       (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign)
   | names, (LocalDef (na,_,_) as decl)::sign ->
-      (PatVar (Loc.ghost,na), decl) :: aux (names,sign)
+      (Loc.tag @@ PatVar na, decl) :: aux (names,sign)
   | _ -> assert false
   in
   List.split (aux (names,sign))
@@ -967,7 +968,7 @@ let use_unit_judge evd =
     evd', j
 
 let add_assert_false_case pb tomatch =
-  let pats = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) tomatch in
+  let pats = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) tomatch in
   let aliasnames =
     List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch
   in
@@ -1165,8 +1166,8 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
 (* Sorting equations by constructor *)
 
 let rec irrefutable env = function
-  | PatVar (_,name) -> true
-  | PatCstr (_,cstr,args,_) ->
+  | _, PatVar name -> true
+  | _, PatCstr (cstr,args,_) ->
       let ind = inductive_of_constructor cstr in
       let (_,mip) = Inductive.lookup_mind_specif env ind in
       let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in
@@ -1187,14 +1188,14 @@ let group_equations pb ind current cstrs mat =
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
 	 match check_and_adjust_constructor pb.env ind cstrs pat with
-	   | PatVar (_,name) ->
+	   | _, PatVar name ->
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
 		 let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
 		 brs.(i-1) <- (args, name, rest) :: brs.(i-1)
 	       done;
 	       if !only_default == None then only_default := Some true
-	   | PatCstr (loc,((_,i)),args,name) ->
+	   | loc, PatCstr (((_,i)),args,name) ->
 	       (* This is a regular clause *)
 	       only_default := Some false;
 	       brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in
@@ -1718,16 +1719,16 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env sigma t Anonymous) avoid in
-    PatVar (Loc.ghost,Name id), ((id,t)::subst, id::avoid) in
+    Loc.tag @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match EConstr.kind sigma (whd_all env sigma t) with
-    | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc
+    | Construct (cstr,u) -> Loc.tag (PatCstr (cstr,[],Anonymous)), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
 	let n = constructor_nrealargs_env env cstr in
 	let l = List.lastn n (Array.to_list v) in
 	let l,acc = List.fold_map' reveal_pattern l acc in
-	PatCstr (Loc.ghost,cstr,l,Anonymous), acc
+	Loc.tag (PatCstr (cstr,l,Anonymous)), acc
     | _ -> make_patvar t acc in
   let rec aux n env acc_sign tms acc =
     match tms with
@@ -1803,7 +1804,7 @@ let build_inversion_problem loc env sigma tms t =
       (* No need for a catch all clause *)
       []
     else
-      [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
+      [ { patterns = List.map (fun _ -> Loc.tag @@ PatVar Anonymous) patl;
           alias_stack = [];
           eqn_loc = Loc.ghost;
           used = ref false;
@@ -2063,18 +2064,18 @@ let hole =
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
-  let rec typ env (ty, realargs) pat avoid =
+  let rec typ env (ty, realargs) (loc, pat) avoid =
     match pat with
-    | PatVar (l,name) ->
+    | PatVar name ->
 	let name, avoid = match name with
 	    Name n -> name, avoid
 	  | Anonymous ->
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
 		Name id, id :: avoid
 	in
-	  (PatVar (l, name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
+	  ((Loc.tag ~loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
-    | PatCstr (l,((_, i) as cstr),args,alias) ->
+    | PatCstr (((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
 	let IndType (indf, _) = 
 	  try find_rectype env ( !evdref) (lift (-(List.length realargs)) ty)
@@ -2083,7 +2084,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	in
 	let (ind,u), params = dest_ind_family indf in
 	let params = List.map EConstr.of_constr params in
-	if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind;
+	if not (eq_ind ind cind) then error_bad_constructor ~loc env cstr ind;
 	let cstrs = get_constructors env indf in
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
@@ -2103,7 +2104,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	in
 	let args = List.rev args in
 	let patargs = List.rev patargs in
-	let pat' = PatCstr (l, cstr, patargs, alias) in
+	let pat' = Loc.tag ~loc @@ PatCstr (cstr, patargs, alias) in
 	let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in
 	let app = applist (cstr, List.map (lift (List.length sign)) params) in
 	let app = applist (app, args) in
@@ -2169,11 +2170,11 @@ let vars_of_ctx sigma ctx =
       ctx (Id.of_string "vars_of_ctx_error", [])
   in List.rev y
 
-let rec is_included x y =
+let rec is_included (loc_x, x) (loc_y, y) =
   match x, y with
     | PatVar _, _ -> true
     | _, PatVar _ -> true
-    | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias')  ->
+    | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias')  ->
 	if Int.equal i i' then List.for_all2 is_included args args'
 	else false
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 542db7fdf..b2c1d0116 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -78,8 +78,9 @@ let apply_coercion_args env evd check isproj argl funj =
 let apply_pattern_coercion loc pat p =
   List.fold_left
     (fun pat (co,n) ->
-       let f i = if i<n then Glob_term.PatVar (loc, Anonymous) else pat in
-	 Glob_term.PatCstr (loc, co, List.init (n+1) f, Anonymous))
+       let f i =
+         if i<n then (Loc.tag ~loc @@ Glob_term.PatVar Anonymous) else pat in
+        Loc.tag ~loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
     pat p
 
 (* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8ba408679..eef6d34ac 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -285,7 +285,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
       (avoid', add_name_opt na' body t env) sigma c
 
 let rec build_tree na isgoal e sigma ci cl =
-  let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name sigma na rhs) in
+  let mkpat n rhs pl = Loc.tag @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
   let cnl = ci.ci_pp_info.cstr_tags in
   let cna = ci.ci_cstr_nargs in
   List.flatten
@@ -308,7 +308,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 	      List.map (fun (hd,rest) -> pat::hd,rest) lines)
 	    clauses)
     | _ ->
-	let pat = PatVar(dl,update_name sigma na rhs) in
+	let pat = Loc.tag @@ PatVar(update_name sigma na rhs) in
 	let mat = align_tree nal isgoal rhs sigma in
 	List.map (fun (hd,rest) -> pat::hd,rest) mat
 
@@ -644,17 +644,17 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
 and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
   let make_pat x avoid env b body ty ids =
     if force_wildcard () && noccurn sigma 1 b then
-      PatVar (dl,Anonymous),avoid,(add_name Anonymous body ty env),ids
+      Loc.tag @@ PatVar (Anonymous),avoid,(add_name Anonymous body ty env),ids
     else
       let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
       let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
-      PatVar (dl,na),avoid',(add_name na body ty env),add_vname ids na
+      Loc.tag @@ PatVar na,avoid',(add_name na body ty env),add_vname ids na
   in
   let rec buildrec ids patlist avoid env l b =
     match EConstr.kind sigma b, l with
       | _, [] ->
         (dl, Id.Set.elements ids,
-         [PatCstr(dl, constr, List.rev patlist,Anonymous)],
+         [Loc.tag ~loc:dl @@ PatCstr(constr, List.rev patlist,Anonymous)],
          detype flags avoid env sigma b)
       | Lambda (x,t,b), false::l ->
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in
@@ -668,7 +668,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
 	    buildrec ids patlist avoid env l c
 
       | _, true::l ->
-	    let pat = PatVar (dl,Anonymous) in
+	    let pat = Loc.tag ~loc:dl @@ PatVar Anonymous in
             buildrec ids (pat::patlist) avoid env l b
 
       | _, false::l ->
@@ -793,14 +793,14 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)
 
-let rec subst_cases_pattern subst pat =
+let rec subst_cases_pattern subst (loc, pat) = Loc.tag ~loc @@
   match pat with
   | PatVar _ -> pat
-  | PatCstr (loc,((kn,i),j),cpl,n) ->
+  | PatCstr (((kn,i),j),cpl,n) ->
       let kn' = subst_mind subst kn
       and cpl' = List.smartmap (subst_cases_pattern subst) cpl in
 	if kn' == kn && cpl' == cpl then pat else
-	  PatCstr (loc,((kn',i),j),cpl',n)
+	  PatCstr (((kn',i),j),cpl',n)
 
 let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
@@ -910,8 +910,8 @@ let rec subst_glob_constr subst raw =
 let simple_cases_matrix_of_branches ind brs =
   List.map (fun (i,n,b) ->
       let nal,c = it_destRLambda_or_LetIn_names n b in
-      let mkPatVar na = PatVar (Loc.ghost,na) in
-      let p = PatCstr (Loc.ghost,(ind,i+1),List.map mkPatVar nal,Anonymous) in
+      let mkPatVar na = Loc.tag @@ PatVar na in
+      let p = Loc.tag @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
       let map name = try Some (Nameops.out_name name) with Failure _ -> None in
       let ids = List.map_filter map nal in
       (Loc.ghost,ids,[p],c))
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index ebbfa195f..27ceabf4e 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -15,9 +15,7 @@ open Glob_term
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
 
-let cases_pattern_loc = function
-    PatVar(loc,_) -> loc
-  | PatCstr(loc,_,_,_) -> loc
+let cases_pattern_loc (loc, _) = loc
 
 let cases_predicate_names tml =
   List.flatten (List.map (function
@@ -47,9 +45,9 @@ let case_style_eq s1 s2 = match s1, s2 with
 | RegularStyle, RegularStyle -> true
 | _ -> 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 (_loc1, p1) (_loc2, 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
@@ -423,18 +421,19 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple =
   if r == inp then x
   else c,(f na, r)
 
-let rec map_case_pattern_binders f = function
-  | PatVar (loc,na) as x ->
+let rec map_case_pattern_binders f = Loc.map (function
+  | PatVar na as x ->
       let r = f na in
       if r == na then x
-      else PatVar (loc,r)
-  | PatCstr (loc,c,ps,na) as x ->
+      else PatVar r
+  | PatCstr (c,ps,na) as x ->
       let rna = f na in
       let rps =
         CList.smartmap (fun p -> map_case_pattern_binders f p) ps
       in
       if rna == na && rps == ps then x
-      else PatCstr(loc,c,rps,rna)
+      else PatCstr(c,rps,rna)
+  )
 
 let map_cases_branch_binders f ((loc,il,cll,rhs) as x) : cases_clause =
   (* spiwack: not sure if I must do something with the list of idents.
@@ -558,26 +557,27 @@ let rec cases_pattern_of_glob_constr na = function
     | Name _ ->
       (* Unable to manage the presence of both an alias and a variable *)
       raise Not_found
-    | Anonymous -> PatVar (loc,Name id)
+    | Anonymous -> Loc.tag ~loc @@ PatVar (Name id)
     end
-  | GHole (loc,_,_,_) -> PatVar (loc,na)
+  | GHole (loc,_,_,_) -> Loc.tag ~loc @@ PatVar na
   | GRef (loc,ConstructRef cstr,_) ->
-      PatCstr (loc,cstr,[],na)
+      Loc.tag ~loc @@ PatCstr (cstr,[],na)
   | GApp (loc,GRef (_,ConstructRef cstr,_),l) ->
-      PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+      Loc.tag ~loc @@ PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
   | _ -> raise Not_found
 
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux = function
-  | PatCstr (loc,cstr,[],Anonymous) ->
+let rec glob_constr_of_closed_cases_pattern_aux x = Loc.with_loc (fun ~loc -> function
+  | PatCstr (cstr,[],Anonymous) ->
       GRef (loc,ConstructRef cstr,None)
-  | PatCstr (loc,cstr,l,Anonymous) ->
+  | PatCstr (cstr,l,Anonymous) ->
       let ref = GRef (loc,ConstructRef cstr,None) in
       GApp (loc,ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
+  ) x
 
 let glob_constr_of_closed_cases_pattern = function
-  | PatCstr (loc,cstr,l,na) ->
-      na,glob_constr_of_closed_cases_pattern_aux (PatCstr (loc,cstr,l,Anonymous))
+  | loc, PatCstr (cstr,l,na) ->
+      na,glob_constr_of_closed_cases_pattern_aux (loc, PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b16d04495..8c570dffe 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 -> ()
       | _ ->