[constrexpr] Make patterns use Loc.located for location information

This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.

Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.

Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.

`git grep 'Loc.t \*'` gives an overview of the remaining work to do.

We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.

16 files changed, 232 insertions, 233 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e20704b7f..19be13be7 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -300,32 +300,32 @@ and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   end
 and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
 and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
+and pp_cases_pattern_expr (loc, cpe) =
   match cpe with
-  | CPatAlias (loc, cpe, id) ->
+  | CPatAlias (cpe, id) ->
       xmlApply loc
         (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
           [pp_cases_pattern_expr cpe])
-  | CPatCstr (loc, ref, None, cpel2) ->
+  | CPatCstr (ref, None, cpel2) ->
       xmlApply loc
         (xmlOperator "reference"
            ~attr:["name", Libnames.string_of_reference ref] loc ::
          [Element ("impargs", [], []);
           Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatCstr (loc, ref, Some cpel1, cpel2) ->
+  | CPatCstr (ref, Some cpel1, cpel2) ->
       xmlApply loc
         (xmlOperator "reference"
            ~attr:["name", Libnames.string_of_reference ref] loc ::
          [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
           Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatAtom (loc, optr) ->
+  | CPatAtom optr ->
       let attrs = match optr with
         | None -> []
         | Some r -> ["name", Libnames.string_of_reference r] in
       xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
-  | CPatOr (loc, cpel) ->
+  | CPatOr cpel ->
       xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
-  | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
+  | CPatNotation (n, (subst_constr, subst_rec), cpel) ->
       xmlApply loc
         (xmlOperator "notation" loc ::
           [xmlOperator n loc;
@@ -339,8 +339,8 @@ and pp_cases_pattern_expr cpe =
                        List.map pp_cases_pattern_expr cpel))
                 subst_rec)]);
            Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
-  | CPatPrim (loc, tok) -> pp_token loc tok
-  | CPatRecord (loc, rcl) ->
+  | CPatPrim tok   -> pp_token loc tok
+  | CPatRecord rcl ->
       xmlApply loc
         (xmlOperator "record" loc ::
            List.map (fun (r, cpe) ->
@@ -348,7 +348,7 @@ and pp_cases_pattern_expr cpe =
                ["reference", Libnames.string_of_reference r],
                [pp_cases_pattern_expr cpe]))
            rcl)
-  | CPatDelimiters (loc, delim, cpe) ->
+  | CPatDelimiters (delim, cpe) ->
       xmlApply loc
         (xmlOperator "delimiter" ~attr:["name", delim] loc ::
           [pp_cases_pattern_expr cpe])
@@ -370,7 +370,7 @@ and pp_case_expr (e, name, pat) =
 and pp_branch_expr_list bel =
   xmlWith
     (List.map
-      (fun (_, cpel, e) ->
+      (fun (_, (cpel, e)) ->
         let ppcepl =
           List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
         let ppe = [pp_expr e] in
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff..3ba5d985f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -59,31 +59,31 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
 
 let eq_located f (_, x) (_, y) = f x y
 
-let rec cases_pattern_expr_eq p1 p2 =
+let rec cases_pattern_expr_eq (l1, p1) (l2, p2) =
   if p1 == p2 then true
   else match p1, p2 with
-  | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) ->
+  | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
       Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
-  | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
+  | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
       eq_reference c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
       List.equal cases_pattern_expr_eq b1 b2
-  | CPatAtom(_,r1), CPatAtom(_,r2) ->
+  | CPatAtom(r1), CPatAtom(r2) ->
       Option.equal eq_reference r1 r2
-  | CPatOr (_, a1), CPatOr (_, a2) ->
+  | CPatOr a1, CPatOr a2 ->
       List.equal cases_pattern_expr_eq a1 a2
-  | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) ->
+  | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
     String.equal n1 n2 &&
     cases_pattern_notation_substitution_eq s1 s2 &&
     List.equal cases_pattern_expr_eq l1 l2
-  | CPatPrim(_,i1), CPatPrim(_,i2) ->
+  | CPatPrim i1, CPatPrim i2 ->
       prim_token_eq i1 i2
-  | CPatRecord (_, l1), CPatRecord (_, l2) ->
+  | CPatRecord l1, CPatRecord l2 ->
       let equal (r1, e1) (r2, e2) =
         eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
       in
       List.equal equal l1 l2
-  | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) ->
+  | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
       String.equal s1 s2 && cases_pattern_expr_eq e1 e2
   | _ -> false
 
@@ -183,7 +183,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   Option.equal (eq_located Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
 
-and branch_expr_eq (_, p1, e1) (_, p2, e2) =
+and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
   List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 &&
   constr_expr_eq e1 e2
 
@@ -252,22 +252,9 @@ let constr_loc = function
   | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
 
-let cases_pattern_expr_loc = function
-  | CPatAlias (loc,_,_) -> loc
-  | CPatCstr (loc,_,_,_) -> loc
-  | CPatAtom (loc,_) -> loc
-  | CPatOr (loc,_) -> loc
-  | CPatNotation (loc,_,_,_) -> loc
-  | CPatRecord (loc, _) -> loc
-  | CPatPrim (loc,_) -> loc
-  | CPatDelimiters (loc,_,_) -> loc
-  | CPatCast(loc,_,_) -> loc
-
-let raw_cases_pattern_expr_loc = function
-  | RCPatAlias (loc,_,_) -> loc
-  | RCPatCstr (loc,_,_,_) -> loc
-  | RCPatAtom (loc,_) -> loc
-  | RCPatOr (loc,_) -> loc
+let cases_pattern_expr_loc (l,_) = l
+
+let raw_cases_pattern_expr_loc (l, _) = l
 
 let local_binder_loc = function
   | CLocalAssum ((loc,_)::_,_,t)
@@ -330,7 +317,7 @@ let expand_binders mkC loc bl c =
             let c =
               CCases
                 (loc, LetPatternStyle, None, [(e,None,None)],
-                 [(loc1, [(loc1,[p])], c)])
+                 [(loc1, ([(loc1,[p])], c))])
             in
             (ni :: env, mkC loc ([id],Default Explicit,ty) c)
   in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 59b8b4e5b..7a229856e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -148,11 +148,11 @@ let insert_delimiters e = function
 
 let insert_pat_delimiters loc p = function
   | None -> p
-  | Some sc -> CPatDelimiters (loc,sc,p)
+  | Some sc -> Loc.tag ~loc @@ CPatDelimiters (sc,p)
 
 let insert_pat_alias loc p = function
   | Anonymous -> p
-  | Name id -> CPatAlias (loc,p,id)
+  | Name id -> Loc.tag ~loc @@ CPatAlias (p,id)
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -178,7 +178,7 @@ let extern_reference loc vars l = !my_extern_reference loc vars l
 
 let add_patt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ CPatAtom None) l
 
 let add_cpatt_for_params ind l =
   if !Flags.in_debugger then l else
@@ -190,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args =
   let rec impls_fit l = function
     |[],t -> Some (List.rev_append l t)
     |_,[] -> None
-    |h::t,CPatAtom(_,None)::tt when is_status_implicit h -> impls_fit l (t,tt)
+    |h::t,(_loc, CPatAtom None)::tt when is_status_implicit h -> impls_fit l (t,tt)
     |h::_,_ when is_status_implicit h -> None
     |_::t,hh::tt -> impls_fit (hh::l) (t,tt)
   in let rec aux = function
@@ -237,7 +237,7 @@ let expand_curly_brackets loc mknot ntn l =
   mknot (loc,!ntn',l)
 
 let destPrim = function CPrim(_,t) -> Some t | _ -> None
-let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
+let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None
 
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
@@ -267,15 +267,15 @@ let make_notation loc ntn (terms,termlists,binders as subst) =
       destPrim terms
 
 let make_pat_notation loc ntn (terms,termlists as subst) args =
-  if not (List.is_empty termlists) then CPatNotation (loc,ntn,subst,args) else
+  if not (List.is_empty termlists) then (loc, CPatNotation (ntn,subst,args)) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]),args))
-    (fun (loc,p) -> CPatPrim (loc,p))
+    (fun (loc,ntn,l) -> Loc.tag ~loc @@ CPatNotation (ntn,(l,[]),args))
+    (fun (loc,p)     -> Loc.tag ~loc @@ CPatPrim p)
     destPatPrim terms
 
 let mkPat loc qid l =
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
-  if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l)
+  if List.is_empty l then Loc.tag ~loc @@ CPatAtom (Some qid) else Loc.tag ~loc @@ CPatCstr (qid,None,l)
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -295,7 +295,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	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
-      CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
+      Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
     | _ ->
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       | None -> raise No_match
       | Some key ->
 	let loc = cases_pattern_loc pat in
-	insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
+	insert_pat_alias loc (insert_pat_delimiters loc (Loc.tag ~loc @@ CPatPrim p) key) na
   with No_match ->
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -312,8 +312,8 @@ 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) -> CPatAtom (loc,Some (Ident (loc,id)))
-	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
+	| 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) ->
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
 	  let p =
@@ -327,24 +327,24 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		  | Some c :: q ->
 		    match args with
 		      | [] -> raise No_match
-		      | CPatAtom(_, None) :: tail -> ip q tail acc
+		      | (_loc, CPatAtom(None)) :: tail -> ip q tail acc
 		    (* we don't want to have 'x = _' in our patterns *)
 		      | head :: tail -> ip q tail
 		        ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
 	      in
-	      CPatRecord(loc, List.rev (ip projs args []))
+	      Loc.tag ~loc @@ CPatRecord(List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
                   let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
 		  if !Topconstr.asymmetric_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
-		    then CPatCstr (loc, c, None, args)
-		    else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
+		    then Loc.tag ~loc @@ CPatCstr (c, None, args)
+		    else Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
 		  else
 		    let full_args = add_patt_for_params (fst cstrsp) args in
 		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
-		      |Some true_args -> CPatCstr (loc, c, None, true_args)
-		      |None -> CPatCstr (loc, c, Some full_args, [])
+		      | Some true_args -> Loc.tag ~loc @@ CPatCstr (c, None, true_args)
+		      | None           -> Loc.tag ~loc @@ CPatCstr (c, Some full_args, [])
 	  in insert_pat_alias loc p na
 and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
     (tmp_scope, scopes as allscopes) vars =
@@ -401,8 +401,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
 	  let p = apply_notation_to_pattern loc (ConstructRef cstr)
 	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias loc p na
-	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
-	| PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
+	| PatVar (loc,Anonymous) -> Loc.tag ~loc @@ CPatAtom None
+	| PatVar (loc,Name id)   -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
     with
 	No_match -> extern_notation_pattern allscopes vars t rules
 
@@ -422,7 +422,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
     let c = extern_reference Loc.ghost vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-    CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), [])
+    Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -430,7 +430,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       match availability_of_prim_token p sc scopes with
 	| None -> raise No_match
 	| Some key ->
-	  insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key
+	  insert_pat_delimiters Loc.ghost (Loc.tag @@ CPatPrim p) key
     with No_match ->
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -440,8 +440,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       let c = extern_reference Loc.ghost vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
-	   |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args)
-	   |None -> CPatCstr (Loc.ghost, c, Some args, [])
+	   |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args)
+	   |None           -> Loc.tag @@ CPatCstr (c, Some args, [])
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
@@ -868,7 +868,7 @@ and extern_local_binder scopes vars = function
       (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
-  (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
+  Loc.tag ~loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
    extern inctx scopes vars c)
 
 and extern_notation (tmp_scope,scopes as allscopes) vars t = function
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf..6bf6772c6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -230,7 +230,7 @@ let contract_pat_notation ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | CPatNotation (_,"{ _ }",([a],[]),[]) :: l ->
+    | (_, CPatNotation ("{ _ }",([a],[]),[])) :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -430,17 +430,16 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
-let rec free_vars_of_pat il =
-  function
-  | CPatCstr (loc, c, l1, l2) ->
+let rec free_vars_of_pat il (loc, pt) = match pt with
+  | CPatCstr (c, l1, l2) ->
       let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
       List.fold_left free_vars_of_pat il l2
-  | CPatAtom (loc, ro) ->
+  | CPatAtom ro ->
       begin match ro with
       | Some (Ident (loc, i)) -> (loc, i) :: il
       | Some _ | None -> il
       end
-  | CPatNotation (loc, n, l1, l2) ->
+  | CPatNotation (n, l1, l2) ->
       let il = List.fold_left free_vars_of_pat il (fst l1) in
       List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
   | _ -> anomaly (str "free_vars_of_pat")
@@ -988,10 +987,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out)
+      then let (b,out) = aux i (q,[]) in (b,(Loc.ghost,RCPatAtom(None))::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out)
+      then let (b,out) = aux i (q,l) in (b,(Loc.ghost, RCPatAtom(None))::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1194,14 +1193,14 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let rec subst_pat_iterator y t p = match p with
-  | RCPatAtom (_,id) ->
-    begin match id with Some x when Id.equal x y -> t | _ -> p end
-  | RCPatCstr (loc,id,l1,l2) ->
-     RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
-	       List.map (subst_pat_iterator y t) l2)
-  | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
-  | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
+let rec subst_pat_iterator y t (loc, p) = match p with
+  | RCPatAtom id ->
+    begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ~loc p end
+  | RCPatCstr (id,l1,l2) ->
+     Loc.tag ~loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
+                                    List.map (subst_pat_iterator y t) l2)
+  | RCPatAlias (p,a) -> Loc.tag ~loc @@ RCPatAlias (subst_pat_iterator y t p,a)
+  | RCPatOr pl       -> Loc.tag ~loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
 
 let drop_notations_pattern looked_for =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1250,46 +1249,46 @@ let drop_notations_pattern looked_for =
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
     with Not_found -> None
-  and in_pat top scopes = function
-    | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id)
-    | CPatRecord (loc, l) ->
+  and in_pat top scopes (loc, pt) = match pt with
+    | CPatAlias (p, id) -> Loc.tag ~loc @@ RCPatAlias (in_pat top scopes p, id)
+    | CPatRecord l ->
       let sorted_fields =
-	sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in
+	sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in
       begin match sorted_fields with
-	| None -> RCPatAtom (loc, None)
+	| None -> Loc.tag ~loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
             if !asymmetric_patterns then pl else
-            let pars = List.make n (CPatAtom (loc, None)) in
+            let pars = List.make n (loc, CPatAtom None) in
             List.rev_append pars pl in
 	  match drop_syndef top scopes head pl with
-	    |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
+	    |Some (a,b,c) -> (loc, RCPatCstr(a, b, c))
 	    |None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, head, None, pl) ->
+    | CPatCstr (head, None, pl) ->
       begin
 	match drop_syndef top scopes head pl with
-	  | Some (a,b,c) -> RCPatCstr(loc, a, b, c)
+	  | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr(a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-     | CPatCstr (loc, r, Some expl_pl, pl) ->
+     | CPatCstr (r, Some expl_pl, pl) ->
       let g = try locate (snd (qualid_of_reference r))
 	      with Not_found ->
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
-        RCPatCstr (loc, g, List.map (in_pat false scopes) pl, [])
+        Loc.tag ~loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
       else
         (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
-        RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
+        Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+    | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
       fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
-    | CPatNotation (_,"( _ )",([a],[]),[]) ->
+    | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
-    | CPatNotation (loc, ntn, fullargs,extrargs) ->
+    | CPatNotation (ntn, fullargs,extrargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
       let ((ids',c),df) = Notation.interp_notation loc ntn scopes in
       let (ids',idsl',_) = split_by_type ids' in
@@ -1297,18 +1296,17 @@ let drop_notations_pattern looked_for =
       let substlist = make_subst idsl' argsl in
       let subst = make_subst ids' args in
       in_not top loc scopes (subst,substlist) extrargs c
-    | CPatDelimiters (loc, key, e) ->
+    | CPatDelimiters (key, e) ->
       in_pat top (None,find_delimiters_scope loc key::snd scopes) e
-    | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
-    | CPatAtom (loc, Some id) ->
+    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+    | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
-	  |Some (a,b,c) -> RCPatCstr (loc, a, b, c)
-	  |None -> RCPatAtom (loc, Some (find_pattern_variable id))
+	  | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr (a, b, c)
+	  | None         -> Loc.tag ~loc @@ RCPatAtom (Some (find_pattern_variable id))
       end
-    | CPatAtom (loc,None) -> RCPatAtom (loc,None)
-    | CPatOr (loc, pl) ->
-      RCPatOr (loc,List.map (in_pat top scopes) pl)
+    | CPatAtom None -> Loc.tag ~loc @@ RCPatAtom None
+    | CPatOr pl     -> Loc.tag ~loc @@ RCPatOr (List.map (in_pat top scopes) pl)
     | CPatCast _ ->
       assert false
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
@@ -1322,17 +1320,17 @@ let drop_notations_pattern looked_for =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-	  if Id.equal id ldots_var then RCPatAtom (loc,Some id) else
+	  if Id.equal id ldots_var then Loc.tag ~loc @@ RCPatAtom (Some id) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
       end
     | NRef g ->
       ensure_kind top loc g;
       let (_,argscs) = find_remaining_scopes [] args g in
-      RCPatCstr (loc, g, [], List.map2 (in_pat_sc scopes) argscs args)
+      Loc.tag ~loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      RCPatCstr (loc, g,
+      Loc.tag ~loc @@ RCPatCstr (g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
@@ -1351,7 +1349,7 @@ let drop_notations_pattern looked_for =
          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole _ ->
       let () = assert (List.is_empty args) in
-      RCPatAtom (loc, None)
+      Loc.tag ~loc @@ RCPatAtom None
     | t -> error_invalid_pattern_notation ~loc ()
   in in_pat true
 
@@ -1363,10 +1361,10 @@ let rec intern_pat genv aliases pat =
       (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
   match pat with
-    | RCPatAlias (loc, p, id) ->
+    | loc, RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_pat genv aliases' p
-    | RCPatCstr (loc, head, expl_pl, pl) ->
+    | loc, RCPatCstr (head, expl_pl, pl) ->
       if !asymmetric_patterns then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
@@ -1378,13 +1376,13 @@ let rec intern_pat genv aliases pat =
 	let with_letin, pl2 =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
-    | RCPatAtom (loc, Some id) ->
+    | loc, RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
       (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)])
-    | RCPatAtom (loc, None) ->
+    | loc, RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
       (ids, [asubst, PatVar (loc, alias_of aliases)])
-    | RCPatOr (loc, pl) ->
+    | loc, RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
       let (idsl,pl') = List.split pl' in
@@ -1402,21 +1400,21 @@ let rec intern_pat genv aliases pat =
    of lambdas in the encoding of match in constr. We put this check here and not
    in the parser because it would require to duplicate the levels of the
    [pattern] rule. *)
-let rec check_no_patcast = function
-  | CPatCast (loc,_,_) ->
+let rec check_no_patcast (loc, pt) = match pt with
+  | CPatCast (_,_) ->
      CErrors.user_err ~loc ~hdr:"check_no_patcast"
                            (Pp.strbrk "Casts are not supported here.")
-  | CPatDelimiters(_,_,p)
-  | CPatAlias(_,p,_) -> check_no_patcast p
-  | CPatCstr(_,_,opl,pl) ->
+  | CPatDelimiters(_,p)
+  | CPatAlias(p,_) -> check_no_patcast p
+  | CPatCstr(_,opl,pl) ->
      Option.iter (List.iter check_no_patcast) opl;
      List.iter check_no_patcast pl
-  | CPatOr(_,pl) ->
+  | CPatOr pl ->
      List.iter check_no_patcast pl
-  | CPatNotation(_,_,subst,pl) ->
+  | CPatNotation(_,subst,pl) ->
      check_no_patcast_subst subst;
      List.iter check_no_patcast pl
-  | CPatRecord(_,prl) ->
+  | CPatRecord prl ->
      List.iter (fun (_,p) -> check_no_patcast p) prl
   | CPatAtom _ | CPatPrim _ -> ()
 
@@ -1441,7 +1439,7 @@ let intern_ind_pattern genv scopes pat =
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc
   in
   match no_not with
-    | RCPatCstr (loc, head, expl_pl, pl) ->
+    | loc, RCPatCstr (head, expl_pl, pl) ->
       let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
@@ -1784,7 +1782,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     (ids,List.flatten mpl')
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
-  and intern_eqn n env (loc,lhs,rhs) =
+  and intern_eqn n env (loc,(lhs,rhs)) =
     let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
diff --git a/interp/modintern.ml b/interp/modintern.ml
index d4ade7058..166711659 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -65,17 +65,16 @@ let transl_with_decl env = function
     let ctx = Evd.evar_context_universe_context ectx in
       WithDef (fqid,(c,ctx))
 
-let loc_of_module = function
-  | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
+let loc_of_module (l, _) = l
 
 (* Invariant : the returned kind is never ModAny, and it is
    equal to the input kind when this one isn't ModAny. *)
 
-let rec interp_module_ast env kind = function
+let rec interp_module_ast env kind (loc, m) = match m with
   | CMident qid ->
-      let (mp,kind) = lookup_module_or_modtype kind qid in
+      let (mp,kind) = lookup_module_or_modtype kind (loc,qid) in
       (MEident mp, kind)
-  | CMapply (_,me1,me2) ->
+  | CMapply (me1,me2) ->
       let me1',kind1 = interp_module_ast env kind me1 in
       let me2',kind2 = interp_module_ast env ModAny me2 in
       let mp2 = match me2' with
@@ -85,7 +84,7 @@ let rec interp_module_ast env kind = function
       if kind2 == ModType then
         error_application_to_module_type (loc_of_module me2);
       (MEapply (me1',mp2), kind1)
-  | CMwith (loc,me,decl) ->
+  | CMwith (me,decl) ->
       let me,kind = interp_module_ast env kind me in
       if kind == Module then error_incorrect_with_in_module loc;
       let decl = transl_with_decl env decl in
diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f729..04711808b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -472,11 +472,11 @@ let interp_prim_token =
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
 let rec rcp_of_glob looked_for = function
-  | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
-  | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
+  | GVar (loc,id)     -> Loc.tag ~loc @@ RCPatAtom (Some id)
+  | GHole (loc,_,_,_) -> Loc.tag ~loc @@ RCPatAtom (None)
+  | GRef (loc,g,_)    -> looked_for g; Loc.tag ~loc @@ RCPatCstr (g,[],[])
   | GApp (loc,GRef (_,g,_),l) ->
-    looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+    looked_for g; Loc.tag ~loc @@ RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
   | _ -> raise Not_found
 
 let interp_prim_token_cases_pattern_expr loc looked_for p =
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d3142e7f0..172caa2ca 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -43,22 +43,22 @@ let is_constructor id =
            (Nametab.locate_extended (qualid_of_ident id)))
   with Not_found -> false
 
-let rec cases_pattern_fold_names f a = function
-  | CPatRecord (_, l) ->
+let rec cases_pattern_fold_names f a pt = match snd pt with
+  | CPatRecord l ->
       List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
-  | CPatAlias (_,pat,id) -> f id a
-  | CPatOr (_,patl) ->
+  | CPatAlias (pat,id) -> f id a
+  | CPatOr (patl) ->
       List.fold_left (cases_pattern_fold_names f) a patl
-  | CPatCstr (_,_,patl1,patl2) ->
+  | CPatCstr (_,patl1,patl2) ->
     List.fold_left (cases_pattern_fold_names f)
       (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
-  | CPatNotation (_,_,(patl,patll),patl') ->
+  | CPatNotation (_,(patl,patll),patl') ->
       List.fold_left (cases_pattern_fold_names f)
 	(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
-  | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
-  | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
+  | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
+  | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a
   | CPatPrim _ | CPatAtom _ -> a
-  | CPatCast (loc,_,_) ->
+  | CPatCast ((loc,_),_) ->
      CErrors.user_err ~loc ~hdr:"cases_pattern_fold_names"
                       (Pp.strbrk "Casts are not supported here.")
 
@@ -125,7 +125,7 @@ let fold_constr_expr_with_binders g f n acc = function
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
-      List.fold_right (fun (loc,patl,rhs) acc ->
+      List.fold_right (fun (loc,(patl,rhs)) acc ->
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
   | CLetTuple (loc,nal,(ona,po),b,c) ->
@@ -230,9 +230,9 @@ let map_constr_expr_with_binders g f e = function
   | CPrim _ | CRef _ as x -> x
   | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
-      let bl = List.map (fun (loc,patl,rhs) ->
+      let bl = List.map (fun (loc,(patl,rhs)) ->
         let ids = ids_of_pattern_list patl in
-        (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
+        (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index 49bafadc8..c1de0ce24 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -36,31 +36,33 @@ type prim_token =
   | Numeral of Bigint.bigint (** representation of integer literals that appear in Coq scripts. *)
   | String of string
 
-type raw_cases_pattern_expr =
-  | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
-  | RCPatCstr of Loc.t * Globnames.global_reference
+type raw_cases_pattern_expr_r =
+  | RCPatAlias of raw_cases_pattern_expr * Id.t
+  | RCPatCstr  of Globnames.global_reference
     * raw_cases_pattern_expr list * raw_cases_pattern_expr list
   (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
-  | RCPatAtom of Loc.t * Id.t option
-  | RCPatOr of Loc.t * raw_cases_pattern_expr list
+  | RCPatAtom of Id.t option
+  | RCPatOr of raw_cases_pattern_expr list
+and raw_cases_pattern_expr = raw_cases_pattern_expr_r Loc.located
 
 type instance_expr = Misctypes.glob_level list
 
-type cases_pattern_expr =
-  | CPatAlias of Loc.t * cases_pattern_expr * Id.t
-  | CPatCstr of Loc.t * reference
+type cases_pattern_expr_r =
+  | CPatAlias of cases_pattern_expr * Id.t
+  | CPatCstr  of reference
     * cases_pattern_expr list option * cases_pattern_expr list
   (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
-  | CPatAtom of Loc.t * reference option
-  | CPatOr of Loc.t * cases_pattern_expr list
-  | CPatNotation of Loc.t * notation * cases_pattern_notation_substitution
+  | CPatAtom of reference option
+  | CPatOr   of cases_pattern_expr list
+  | CPatNotation of notation * cases_pattern_notation_substitution
     * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents
 				  (notation n applied with substitution l1)
 				  applied to arguments l2 *)
-  | CPatPrim of Loc.t * prim_token
-  | CPatRecord of Loc.t * (reference * cases_pattern_expr) list
-  | CPatDelimiters of Loc.t * string * cases_pattern_expr
-  | CPatCast of Loc.t * cases_pattern_expr * constr_expr
+  | CPatPrim   of prim_token
+  | CPatRecord of (reference * cases_pattern_expr) list
+  | CPatDelimiters of string * cases_pattern_expr
+  | CPatCast   of cases_pattern_expr * constr_expr
+and cases_pattern_expr = cases_pattern_expr_r located
 
 and cases_pattern_notation_substitution =
     cases_pattern_expr list *     (** for constr subterms *)
@@ -104,7 +106,7 @@ and case_expr = constr_expr                 (* expression that is being matched
 	      * cases_pattern_expr option   (* in-clause *)
 
 and branch_expr =
-  Loc.t * cases_pattern_expr list located list * constr_expr
+  (cases_pattern_expr list located list * constr_expr) Loc.located
 
 and binder_expr =
   Name.t located list * binder_kind * constr_expr
@@ -144,7 +146,8 @@ type with_declaration_ast =
   | CWith_Module of Id.t list located * qualid located
   | CWith_Definition of Id.t list located * constr_expr
 
-type module_ast =
-  | CMident of qualid located
-  | CMapply of Loc.t * module_ast * module_ast
-  | CMwith of Loc.t * module_ast * with_declaration_ast
+type module_ast_r =
+  | CMident of qualid
+  | CMapply of module_ast * module_ast
+  | CMwith  of module_ast * with_declaration_ast
+and module_ast = module_ast_r located
diff --git a/lib/loc.ml b/lib/loc.ml
index e373a760c..39f2d7dfb 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -59,6 +59,10 @@ let join_loc = merge
 (** Located type *)
 
 type 'a located = t * 'a
+
+let to_pair x = x
+let tag ?loc x = Option.default ghost loc, x
+
 let located_fold_left f x (_,a) = f x a
 let located_iter2 f (_,a) (_,b) = f a b
 let down_located f (_,a) = f a
diff --git a/lib/loc.mli b/lib/loc.mli
index bb88f8642..fef1d8938 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -18,9 +18,6 @@ type t = {
   ep : int; (** end position *)
 }
 
-type 'a located = t * 'a
-(** Embed a location in a type *)
-
 (** {5 Location manipulation} *)
 
 (** This is inherited from CAMPL4/5. *)
@@ -54,12 +51,22 @@ val get_loc : Exninfo.info -> t option
 val raise : ?loc:t -> exn -> 'a
 (** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *)
 
-(** {5 Location utilities} *)
+(** {5 Objects with location information } *)
+
+type 'a located = t * 'a
+(** Embed a location in a type *)
+
+(** Warning, this API is experimental  *)
+
+val to_pair : 'a located -> t * 'a
+val tag : ?loc:t -> 'a -> 'a located
 
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val down_located : ('a -> 'b) -> 'a located -> 'b
+
+(* Current not used *)
 val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
 
-val down_located : ('a -> 'b) -> 'a located -> 'b
 (** Projects out a located object *)
 
 (** {5 Backward compatibility} *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 496b20002..a973a539a 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -318,8 +318,8 @@ let constr_expr_of_name (loc,na) = match na with
   | Name id -> CRef (Ident (loc,id), None)
 
 let cases_pattern_expr_of_name (loc,na) = match na with
-  | Anonymous -> CPatAtom (loc,None)
-  | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
+  | Anonymous -> Loc.tag ~loc @@ CPatAtom None
+  | Name id   -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
 
 type 'r env = {
   constrs : 'r list;
@@ -342,13 +342,13 @@ match e with
 | TTBinderListF _ -> { subst with binders = (List.flatten v, false) :: subst.binders }
 | TTBigint ->
   begin match forpat with
-  | ForConstr -> push_constr subst (CPrim (Loc.ghost, Numeral v))
-  | ForPattern -> push_constr subst (CPatPrim (Loc.ghost, Numeral v))
+  | ForConstr ->  push_constr subst (CPrim (Loc.ghost, Numeral v))
+  | ForPattern -> push_constr subst (Loc.tag @@ CPatPrim (Numeral v))
   end
 | TTReference ->
   begin match forpat with
-  | ForConstr -> push_constr subst (CRef (v, None))
-  | ForPattern -> push_constr subst (CPatAtom (Loc.ghost, Some v))
+  | ForConstr  -> push_constr subst (CRef (v, None))
+  | ForPattern -> push_constr subst (Loc.tag @@ CPatAtom (Some v))
   end
 | TTConstrList _ -> { subst with constrlists = v :: subst.constrlists }
 
@@ -436,7 +436,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   let invalid = List.exists (fun (_, b) -> not b) env.binders in
   let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in
   let env = (env.constrs, env.constrlists) in
-  CPatNotation (loc, notation, env, [])
+  Loc.tag ~loc @@ CPatNotation (notation, env, [])
 
 let extend_constr state forpat ng =
   let n = ng.notgram_level in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 0f2ed88fe..6ca8134c0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -120,7 +120,7 @@ let name_colon =
               | _ -> err ())
         | _ -> err ())
 
-let aliasvar = function CPatAlias (loc, _, id) -> Some (loc,Name id) | _ -> None
+let aliasvar = function loc, CPatAlias (_, id) -> Some (loc,Name id) | _ -> None
 
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr universe_level sort global
@@ -254,14 +254,14 @@ GEXTEND Gram
           CLetTuple (!@loc,lb,po,c1,c2)
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, None, [c1, None, None], [(!@loc, [(!@loc,[p])], c2)])
+	    CCases (!@loc, LetPatternStyle, None,    [c1, None, None],       [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200";
 	  rt = case_type; "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
       | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200";
 	  ":="; c1 = operconstr LEVEL "200"; rt = case_type;
           "in"; c2 = operconstr LEVEL "200" ->
-	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [(!@loc, [(!@loc, [p])], c2)])
+	    CCases (!@loc, LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(!@loc, [p])], c2)])
       | "if"; c=operconstr LEVEL "200"; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
         "else"; b2=operconstr LEVEL "200" ->
@@ -349,7 +349,7 @@ GEXTEND Gram
   ;
   eqn:
     [ [ pll = LIST1 mult_pattern SEP "|";
-        "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
+        "=>"; rhs = lconstr -> (Loc.tag ~loc:!@loc (pll,rhs)) ] ]
   ;
   record_pattern:
     [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
@@ -364,46 +364,46 @@ GEXTEND Gram
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
-      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CPatOr (!@loc,p::pl) ]
+      [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> !@loc, CPatOr (p::pl) ]
     | "99" RIGHTA [ ]
     | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
-	  CPatAlias (!@loc, p, id) ]
+        Loc.tag ~loc:!@loc @@ CPatAlias (p, id) ]
     | "10" RIGHTA
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
-	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
-	  | CPatCstr (_, r, None, l2) -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
-              (Pp.str "Nested applications not supported.")
-	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
-	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
+	  | _,   CPatAtom (Some r) -> Loc.tag ~loc:!@loc @@ CPatCstr (r, None, lp)
+	  | loc, CPatCstr (r, None, l2) ->
+                 CErrors.user_err ~loc ~hdr:"compound_pattern"
+                 (Pp.str "Nested applications not supported.")
+	  | _,   CPatCstr (r, l1, l2)   -> Loc.tag ~loc:!@loc @@ CPatCstr (r, l1 , l2@lp)
+	  | _,   CPatNotation (n, s, l) -> Loc.tag ~loc:!@loc @@ CPatNotation (n , s, l@lp)
           | _ -> CErrors.user_err
               ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
               (Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
-        CPatCstr (!@loc, r, Some lp, []) ]
+        !@loc, CPatCstr (r, Some lp, []) ]
     | "1" LEFTA
-      [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
+      [ c = pattern; "%"; key=IDENT -> !@loc, CPatDelimiters (key,c) ]
     | "0"
-      [ r = Prim.reference -> CPatAtom (!@loc,Some r)
-      | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
-      | "_" -> CPatAtom (!@loc,None)
+      [ r = Prim.reference                -> Loc.tag ~loc:!@loc @@ CPatAtom (Some r)
+      | "{|"; pat = record_patterns; "|}" -> Loc.tag ~loc:!@loc @@ CPatRecord pat
+      | "_" -> !@loc, CPatAtom None
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
-              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CPatNotation(!@loc,"( _ )",([p],[]),[])
+            | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+                 Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p)
       | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" ->
           let p =
             match p with
-              CPatPrim (_,Numeral z) when Bigint.is_pos_or_zero z ->
-                CPatNotation(!@loc,"( _ )",([p],[]),[])
+            | _, CPatPrim (Numeral z) when Bigint.is_pos_or_zero z ->
+                 Loc.tag ~loc:!@loc @@ CPatNotation("( _ )",([p],[]),[])
             | _ -> p
           in
-	  CPatCast (!@loc, p, ty)
-      | n = INT -> CPatPrim (!@loc, Numeral (Bigint.of_string n))
-      | s = string -> CPatPrim (!@loc, String s) ] ]
+	  !@loc, CPatCast (p, ty)
+      | n = INT    -> Loc.tag ~loc:!@loc @@ CPatPrim (Numeral (Bigint.of_string n))
+      | s = string -> Loc.tag ~loc:!@loc @@ CPatPrim (String s) ] ]
   ;
   impl_ident_tail:
     [ [ "}" -> binder_of_name Implicit
@@ -482,7 +482,7 @@ GEXTEND Gram
       | "'"; p = pattern LEVEL "0" ->
           let (p, ty) =
             match p with
-            | CPatCast (_, p, ty) -> (p, Some ty)
+            | _, CPatCast (p, ty) -> (p, Some ty)
             | _ -> (p, None)
           in
           [CLocalPattern (!@loc, p, ty)]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 011565d86..a43f1127a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -511,11 +511,11 @@ GEXTEND Gram
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> me
-      | me1 = module_expr; me2 = module_expr_atom -> CMapply (!@loc,me1,me2)
+      | me1 = module_expr; me2 = module_expr_atom -> Loc.tag ~loc:!@loc @@ CMapply (me1,me2)
       ] ]
   ;
   module_expr_atom:
-    [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ]
+    [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ]
   ;
   with_declaration:
     [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr ->
@@ -525,11 +525,12 @@ GEXTEND Gram
       ] ]
   ;
   module_type:
-    [ [ qid = qualid -> CMident qid
+    [ [ qid = qualid -> Loc.tag ~loc:!@loc @@ CMident (snd qid)
       | "("; mt = module_type; ")" -> mt
-      | mty = module_type; me = module_expr_atom -> CMapply (!@loc,mty,me)
+      | mty = module_type; me = module_expr_atom ->
+          Loc.tag ~loc:!@loc @@ CMapply (mty,me)
       | mty = module_type; "with"; decl = with_declaration ->
-          CMwith (!@loc,mty,decl)
+          Loc.tag ~loc:!@loc @@ CMwith (mty,decl)
       ] ]
   ;
   (* Proof using *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d335836df..daa5cbb3f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -760,7 +760,7 @@ let rec add_args id new_args b =
 	     List.map (fun (b,na,b_option) ->
 			 add_args id new_args b,
 			 na, b_option) cel,
-	     List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
+	     List.map (fun (loc,(cpl,e)) -> Loc.tag ~loc:loc @@ (cpl,add_args id new_args e)) cal
 	    )
   | CLetTuple(loc,nal,(na,b_option),b1,b2) ->
       CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 38eeda9b9..966ba6734 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -252,62 +252,62 @@ let tag_var = tag Tag.variable
   let lpator = 100
   let lpatrec = 0
 
-  let rec pr_patt sep inh p =
+  let rec pr_patt sep inh (loc, p) =
     let (strm,prec) = match p with
-      | CPatRecord (_, l) ->
+      | CPatRecord l ->
         let pp (c, p) =
           pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
         in
         str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
 
-      | CPatAlias (_, p, id) ->
+      | CPatAlias (p, id) ->
         pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
 
-      | CPatCstr (_,c, None, []) ->
+      | CPatCstr (c, None, []) ->
         pr_reference c, latom
 
-      | CPatCstr (_, c, None, args) ->
+      | CPatCstr (c, None, args) ->
         pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
 
-      | CPatCstr (_, c, Some args, []) ->
+      | CPatCstr (c, Some args, []) ->
         str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
 
-      | CPatCstr (_, c, Some expl_args, extra_args) ->
+      | CPatCstr (c, Some expl_args, extra_args) ->
         surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
         ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
 
-      | CPatAtom (_, None) ->
+      | CPatAtom (None) ->
         str "_", latom
 
-      | CPatAtom (_,Some r) ->
+      | CPatAtom (Some r) ->
         pr_reference r, latom
 
-      | CPatOr (_,pl) ->
+      | CPatOr pl ->
         hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator
 
-      | CPatNotation (_,"( _ )",([p],[]),[]) ->
+      | CPatNotation ("( _ )",([p],[]),[]) ->
         pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
 
-      | CPatNotation (_,s,(l,ll),args) ->
+      | CPatNotation (s,(l,ll),args) ->
         let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ _ -> mt()) s (l,ll,[]) in
         (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
         ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
 
-      | CPatPrim (_,p) ->
+      | CPatPrim p ->
         pr_prim_token p, latom
 
-      | CPatDelimiters (_,k,p) ->
+      | CPatDelimiters (k,p) ->
         pr_delimiters k (pr_patt mt lsimplepatt p), 1
       | CPatCast _ ->
         assert false
     in
-    let loc = cases_pattern_expr_loc p in
+    let loc = cases_pattern_expr_loc (loc, p) in
     pr_with_comments loc
       (sep() ++ if prec_less prec inh then strm else surround strm)
 
   let pr_patt = pr_patt mt
 
-  let pr_eqn pr (loc,pl,rhs) =
+  let pr_eqn pr (loc,(pl,rhs)) =
     let pl = List.map snd pl in
     spc() ++ hov 4
       (pr_with_comments loc
@@ -397,7 +397,7 @@ let tag_var = tag Tag.variable
     | CProdN (loc,[],c) ->
       extract_prod_binders c
     | CProdN (loc,[[_,Name id],bk,t],
-              CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+              CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_prod_binders b in
       CLocalPattern (loc,p,None) :: bl, c
@@ -413,7 +413,7 @@ let tag_var = tag Tag.variable
     | CLambdaN (loc,[],c) ->
       extract_lam_binders c
     | CLambdaN (loc,[[_,Name id],bk,t],
-                CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+                CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,([_,[p]],b))]))
          when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
       let bl,c = extract_lam_binders b in
       CLocalPattern (loc,p,None) :: bl, c
@@ -642,7 +642,7 @@ let tag_var = tag Tag.variable
           hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
           latom
         )
-      | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,[(loc,[p])],b)]) ->
+      | CCases (_,LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e4a87739b..2e064454c 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -204,18 +204,18 @@ open Decl_kinds
         pr_located pr_qualid qid
 
   let rec pr_module_ast leading_space pr_c = function
-    | CMident qid ->
+    | loc, CMident qid ->
       if leading_space then
-        spc () ++ pr_located pr_qualid qid
+        spc () ++ pr_located pr_qualid (loc, qid)
       else
-        pr_located pr_qualid qid
-    | CMwith (_,mty,decl) ->
+        pr_located pr_qualid (loc,qid)
+    | _loc, CMwith (mty,decl) ->
       let m = pr_module_ast leading_space pr_c mty in
       let p = pr_with_declaration pr_c decl in
       m ++ spc() ++ keyword "with" ++ spc() ++ p
-    | CMapply (_,me1,(CMident _ as me2)) ->
+    | _loc, CMapply (me1,(_, CMident _ as me2)) ->
       pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2
-    | CMapply (_,me1,me2) ->
+    | _loc, CMapply (me1,me2) ->
       pr_module_ast leading_space pr_c me1 ++ spc() ++
         hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")")