[ast] Improve precision of Ast location recognition in serialization.

We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.

With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.

18 files changed, 161 insertions, 146 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 7d2c4d082..794a28dd4 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -346,7 +346,7 @@ let () = register_list_tactical "solve" Tacticals.New.tclSOLVE
 
 let initial_tacticals () =
   let idn n = Id.of_string (Printf.sprintf "_%i" n) in
-  let varn n = Reference (ArgVar (None, idn n)) in
+  let varn n = Reference (ArgVar (CAst.make (idn n))) in
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
   List.iter iter [
     "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 4c6d3c2d3..2eb1ef315 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -81,7 +81,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l
 let pr_occurrences _prc _prlc _prt l =
   match l with
     | ArgArg x -> pr_int_list x
-    | ArgVar (loc, id) -> Id.print id
+    | ArgVar { CAst.loc = loc; v=id } -> Id.print id
 
 let occurrences_of = function
   | [] -> NoOccurrences
@@ -102,7 +102,7 @@ let int_list_of_VList v = match Value.to_list v with
 let interp_occs ist gl l =
   match l with
     | ArgArg x -> x
-    | ArgVar (_,id as locid) ->
+    | ArgVar ({ CAst.v = id } as locid) ->
 	(try int_list_of_VList (Id.Map.find id ist.lfun)
 	  with Not_found | CannotCoerceTo _ -> [interp_int ist locid])
 let interp_occs ist gl l =
@@ -188,7 +188,7 @@ END
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
-type loc_place = Id.t Loc.located gen_place
+type loc_place = lident gen_place
 type place = Id.t gen_place
 
 let pr_gen_place pr_id = function
@@ -199,7 +199,7 @@ let pr_gen_place pr_id = function
   | HypLocation (id,InHypValueOnly) ->
       str "in (Value of " ++ pr_id id ++ str ")"
 
-let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id)
+let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id)
 let pr_place _ _ _ = pr_gen_place Id.print
 let pr_hloc = pr_loc_place () () ()
 
@@ -228,11 +228,11 @@ ARGUMENT EXTEND hloc
   |  [ "in" "|-" "*" ] ->
     [ ConclLocation () ]
 | [ "in" ident(id) ] ->
-    [ HypLocation ((Loc.tag id),InHyp) ]
+    [ HypLocation ((CAst.make id),InHyp) ]
 | [ "in" "(" "Type" "of" ident(id) ")" ] ->
-    [ HypLocation ((Loc.tag id),InHypTypeOnly) ]
+    [ HypLocation ((CAst.make id),InHypTypeOnly) ]
 | [ "in" "(" "Value" "of" ident(id) ")" ] ->
-    [ HypLocation ((Loc.tag id),InHypValueOnly) ]
+    [ HypLocation ((CAst.make id),InHypValueOnly) ]
 
  END
 
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 00668ddc7..000c3d2fb 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -50,7 +50,7 @@ val lglob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 
-type loc_place = Id.t Loc.located gen_place
+type loc_place = lident gen_place
 type place = Id.t gen_place
 
 val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
@@ -77,6 +77,6 @@ val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
 val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
 
 val wit_in_clause :
-  (Id.t Loc.located Locus.clause_expr,
-  Id.t Loc.located Locus.clause_expr,
-  Id.t Locus.clause_expr) Genarg.genarg_type
+  (lident Locus.clause_expr,
+   lident Locus.clause_expr,
+   Id.t   Locus.clause_expr) Genarg.genarg_type
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 286f9d95d..10be8a842 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -71,7 +71,7 @@ END
 
 let induction_arg_of_quantified_hyp = function
   | AnonHyp n -> None,ElimOnAnonHyp n
-  | NamedHyp id -> None,ElimOnIdent (Loc.tag id)
+  | NamedHyp id -> None,ElimOnIdent (CAst.make id)
 
 (* Versions *_main must come first!! so that "1" is interpreted as a
    ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 9ef819569..85c9fc5fd 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -37,10 +37,10 @@ let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
 let reference_to_id = function
-  | Libnames.Ident (loc, id) -> (loc, id)
+  | Libnames.Ident (loc, id) -> CAst.make ?loc id
   | Libnames.Qualid (loc,_) ->
-      CErrors.user_err ?loc 
-       (str "This expression should be a simple identifier.")
+    CErrors.user_err ?loc
+      (str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
 
@@ -196,7 +196,7 @@ GEXTEND Gram
      verbose most of the time. *)
   fresh_id:
     [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
-	| qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ]
+        | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
@@ -225,12 +225,12 @@ GEXTEND Gram
       | l = ident -> Name.Name l ] ]
   ;
   let_clause:
-    [ [ (l,id) = identref; ":="; te = tactic_expr ->
-         ((l,Name id), arg_of_expr te)
-      | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr ->
+    [ [ idr = identref; ":="; te = tactic_expr ->
+         (CAst.map (fun id -> Name id) idr, arg_of_expr te)
+      | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr ->
          (na, arg_of_expr te)
-      | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
-         ((l,Name id), arg_of_expr (TacFun(args,te))) ] ]
+      | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr ->
+         (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ]
   ;
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
@@ -483,7 +483,7 @@ let pr_ltac_ref = Libnames.pr_reference
 let pr_tacdef_body tacdef_body =
   let id, redef, body =
     match tacdef_body with
-    | TacticDefinition ((_,id), body) -> Id.print id, false, body
+    | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body
     | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
   in
   let idl, body =
@@ -504,7 +504,7 @@ END
 VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
 | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
     VtSideff (List.map (function
-      | TacticDefinition ((_,r),_) -> r
+      | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (Ident (_,r),_) -> r
       | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
   ] -> [ fun ~atts ~st -> let open Vernacinterp in
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index e68140828..338d61e6f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -115,16 +115,16 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
     match bl,ann with
         [([_],_,_)], None -> 1
       | _, Some x ->
-          let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
-          (try List.index Names.Name.equal (snd x) ids
+          let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
+          (try List.index Names.Name.equal x.CAst.v ids
           with Not_found -> user_err Pp.(str "No such fix variable."))
       | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
   let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
   (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
-  let _ = Option.map (fun (aloc,_) ->
-    user_err ~loc:aloc
+  let _ = Option.map (fun { CAst.loc = aloc } ->
+    user_err ?loc:aloc
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
   let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
@@ -134,7 +134,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
 let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
   | NoBindings ->
     begin
-      try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c))
+      try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v)
       with e when CErrors.noncritical e -> ElimOnConstr clbind
     end
   | _ -> ElimOnConstr clbind
@@ -152,6 +152,7 @@ let mkTacCase with_evar = function
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
+    let id = CAst.(id.loc, id.v) in
       TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
@@ -161,7 +162,7 @@ let mkTacCase with_evar = function
 
 let rec mkCLambdaN_simple_loc ?loc bll c =
   match bll with
-  | ((loc1,_)::_ as idl,bk,t) :: bll ->
+  | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll ->
       CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
   | [] -> c
@@ -169,7 +170,7 @@ let rec mkCLambdaN_simple_loc ?loc bll c =
 let mkCLambdaN_simple bl c = match bl with
   | [] -> c
   | h :: _ ->
-    let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in
+    let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in
     mkCLambdaN_simple_loc ?loc bl c
 
 let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
@@ -381,15 +382,20 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta ->
-          id,InHyp
+        let id : Misctypes.lident = id in
+        id,InHyp
       | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
-	  id,InHypTypeOnly
+        let id : Misctypes.lident = id in
+        id,InHypTypeOnly
       | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
-	  id,InHypValueOnly
+        let id : Misctypes.lident = id in
+        id,InHypValueOnly
     ] ]
   ;
   hypident_occ:
-    [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ]
+    [ [ (id,l)=hypident; occs=occs ->
+        let id : Misctypes.lident = id in
+        ((occs,id),l) ] ]
   ;
   in_clause:
     [ [ "*"; occs=occs ->
@@ -433,7 +439,8 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+    [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@
+                    CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))
       | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
     ] ]
   ;
@@ -565,28 +572,34 @@ GEXTEND Gram
           TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
 
       (* Alternative syntax for "pose proof c as id" *)
-      | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+      | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
-      | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+          let { CAst.loc = loc; v = id } = lid in
+          TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+          let { CAst.loc = loc; v = id } = lid in
+          TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "assert c as id by tac" *)
-      | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+      | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
-      | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+          let { CAst.loc = loc; v = id } = lid in
+          TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+          let { CAst.loc = loc; v = id } = lid in
+          TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "enough c as id by tac" *)
-      | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+      | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
-      | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+          let { CAst.loc = loc; v = id } = lid in
+          TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+          let { CAst.loc = loc; v = id } = lid in
+          TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
 	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 048dcc8e9..ecb0b5796 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -9,7 +9,6 @@
 (** Ltac parsing entries *)
 
 open Loc
-open Names
 open Pcoq
 open Libnames
 open Constrexpr
@@ -20,7 +19,7 @@ open Misctypes
 val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
 val bindings : constr_expr bindings Gram.entry
-val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
+val hypident : (lident * Locus.hyp_location_flag) Gram.entry
 val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
@@ -29,8 +28,8 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
 val int_or_var : int or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
 val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
-val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry
-val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry
+val in_clause : lident Locus.clause_expr Gram.entry
+val clause_dft_concl : lident Locus.clause_expr Gram.entry
 val tactic_arg : raw_tactic_arg Gram.entry
 val tactic_expr : raw_tactic_expr Gram.entry
 val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4f430b79e..3bc9f2aa0 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -161,7 +161,7 @@ let string_of_genarg_arg (ArgumentType arg) =
         (keyword "eval" ++ brk (1,1) ++
            pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
            keyword "in" ++ spc() ++ prc c)
-    | ConstrContext ((_,id),c) ->
+    | ConstrContext ({CAst.v=id},c) ->
       hov 0
         (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
            str "[ " ++ prlc c ++ str " ]")
@@ -364,7 +364,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_ltac_or_var pr = function
     | ArgArg x -> pr x
-    | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id)
+    | ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id)
 
   let pr_ltac_constant kn =
     if !Flags.in_debugger then KerName.print kn
@@ -404,7 +404,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_as_name = function
     | Anonymous -> mt ()
-    | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id)
+    | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (CAst.make id)
 
   let pr_pose_as_style prc na c =
     spc() ++ prc c ++ pr_as_name na
@@ -496,12 +496,12 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_core_destruction_arg prc prlc = function
     | ElimOnConstr c -> pr_with_bindings prc prlc c
-    | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id)
+    | ElimOnIdent {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id)
     | ElimOnAnonHyp n -> int n
 
   let pr_destruction_arg prc prlc (clear_flag,h) =
     pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
-                               
+
   let pr_inversion_kind = function
     | SimpleInversion -> primitive "simple inversion"
     | FullInversion -> primitive "inversion"
@@ -684,7 +684,7 @@ let pr_goal_selector ~toplevel s =
         (*  match t with
             | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
             | _ ->*)
-        let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+        let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
         spc() ++ hov 1 (str"(" ++ s ++ str")") in
 
       let pr_fix_tac (id,n,c) =
@@ -692,10 +692,10 @@ let pr_goal_selector ~toplevel s =
         (nal,ty)::bll ->
           if n <= List.length nal then
             match List.chop (n-1) nal with
-                _, (_,Name id) :: _ -> id, (nal,ty)::bll
-              | bef, (loc,Anonymous) :: aft ->
+                _, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll
+              | bef, {CAst.loc;v=Anonymous} :: aft ->
                 let id = next_ident_away (Id.of_string"y") avoid in
-                id, ((bef@(loc,Name id)::aft, ty)::bll)
+                id, ((bef@(CAst.make ?loc @@ Name id)::aft, ty)::bll)
               | _ -> assert false
           else
             let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
@@ -705,7 +705,7 @@ let pr_goal_selector ~toplevel s =
         let names =
           List.fold_left
             (fun ln (nal,_) -> List.fold_left
-              (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln)
+              (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln)
               ln nal)
             Id.Set.empty bll in
         let idarg,bll = set_nth_name names n bll in
@@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
         match DAst.get ty with
             Glob_term.GProd(na,Explicit,a,b) ->
-              strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
+              strip_ty (([CAst.make na],(a,None))::acc) (n-1) b
           | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
@@ -1158,7 +1158,7 @@ let pr_goal_selector ~toplevel s =
       if n=0 then (List.rev acc, EConstr.of_constr ty) else
         match Constr.kind ty with
         | Constr.Prod(na,a,b) ->
-          strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
+          strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b
         | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
@@ -1318,7 +1318,7 @@ let () =
   register_basic_print0 wit_ref
     pr_reference (pr_or_var (pr_located pr_global)) pr_global;
   register_basic_print0 wit_ident pr_id pr_id pr_id;
-  register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id;
+  register_basic_print0 wit_var pr_lident pr_lident pr_id;
   register_print0
     wit_intro_pattern
     (lift (Miscprint.pr_intro_pattern pr_constr_expr))
@@ -1328,7 +1328,7 @@ let () =
     wit_clause_dft_concl
     (lift (pr_clauses (Some true) pr_lident))
     (lift (pr_clauses (Some true) pr_lident))
-    (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
+    (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c))
   ;
   Genprint.register_print0
     wit_constr
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index acd7a30c4..e73a18b79 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1773,7 +1773,7 @@ let rec strategy_of_ast = function
 let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
-  (((Loc.tag @@ Name n),None), Explicit,
+  (((CAst.make @@ Name n),None), Explicit,
   CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@  qualid_of_string s),None),
 	   args))
 
@@ -2006,7 +2006,7 @@ let add_morphism glob binders m s n =
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
-    (((Loc.tag @@ Name instance_id),None), Explicit,
+    (((CAst.make @@ Name instance_id),None), Explicit,
     CAst.make @@ CAppExpl (
 	     (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 8112cc400..4313456a4 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -374,7 +374,7 @@ let add_ml_tactic_notation name ~level prods =
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
-    let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in
+    let map id = Reference (Misctypes.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
     add_glob_tactic_notation false ~level prods true ids tac
   in
@@ -431,11 +431,11 @@ let warn_unusable_identifier =
 let register_ltac local tacl =
   let map tactic_body =
     match tactic_body with
-    | Tacexpr.TacticDefinition ((loc,id), body) ->
+    | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
         let kn = Lib.make_kn id in
         let id_pp = Id.print id in
         let () = if is_defined_tac kn then
-          CErrors.user_err ?loc 
+          CErrors.user_err ?loc
             (str "There is already an Ltac named " ++ id_pp ++ str".")
         in
         let is_shadowed =
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index ccd555b61..146d8300d 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -41,7 +41,7 @@ type goal_selector = Vernacexpr.goal_selector =
 
 type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
   | ElimOnConstr of 'a
-  | ElimOnIdent of Id.t located
+  | ElimOnIdent of lident
   | ElimOnAnonHyp of int
 
 type 'a destruction_arg =
@@ -85,8 +85,8 @@ type 'a match_pattern =
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
-  | Hyp of Name.t located * 'a match_pattern
-  | Def of Name.t located * 'a match_pattern * 'a match_pattern
+  | Hyp of lname * 'a match_pattern
+  | Def of lname * 'a match_pattern * 'a match_pattern
 
 (* Type of a Match rule for Match Context and Match *)
 type ('a,'t) match_rule =
@@ -254,7 +254,7 @@ and 'a gen_tactic_expr =
   | TacFail of global_flag * int or_var * 'n message_token list
   | TacInfo of 'a gen_tactic_expr
   | TacLetIn of rec_flag *
-      (Name.t located * 'a gen_tactic_arg) list *
+      (lname * 'a gen_tactic_arg) list *
       'a gen_tactic_expr
   | TacMatch of lazy_flag *
       'a gen_tactic_expr *
@@ -300,7 +300,7 @@ type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
 type g_cst = evaluable_global_reference and_short_name or_var
 type g_ref = ltac_constant located or_var
-type g_nam  = Id.t located
+type g_nam = lident
 
 type g_dispatch =  <
     term:g_trm;
@@ -328,7 +328,7 @@ type r_trm = constr_expr
 type r_pat = constr_pattern_expr
 type r_cst = reference or_by_notation
 type r_ref = reference
-type r_nam  = Id.t located
+type r_nam = lident
 type r_lev = rlevel
 
 type r_dispatch =  <
@@ -357,7 +357,7 @@ type t_trm = EConstr.constr
 type t_pat = constr_pattern
 type t_cst = evaluable_global_reference
 type t_ref = ltac_constant located
-type t_nam  = Id.t
+type t_nam = Id.t
 
 type t_dispatch =  <
     term:t_trm;
@@ -391,5 +391,5 @@ type ltac_call_kind =
 type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
-  | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
+  | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
   | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ebffde441..22ec6c5b1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,12 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pattern
 open Pp
+open CErrors
+open CAst
+open Pattern
 open Genredexpr
 open Glob_term
 open Tacred
-open CErrors
 open Util
 open Names
 open Libnames
@@ -73,11 +74,11 @@ let strict_check = ref false
 let adjust_loc loc = if !strict_check then None else loc
 
 (* Globalize a name which must be bound -- actually just check it is bound *)
-let intern_hyp ist (loc,id as locid) =
+let intern_hyp ist ({loc;v=id} as locid) =
   if not !strict_check then
     locid
   else if find_ident id ist then
-    Loc.tag id
+    make id
   else
     Pretype_errors.error_var_not_found ?loc id
 
@@ -89,7 +90,8 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n)
 let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 
 let intern_global_reference ist = function
-  | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
+  | Ident (loc,id) when find_var id ist ->
+    ArgVar CAst.(make ?loc id)
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       try ArgArg (loc,locate_global_with_alias lqid)
@@ -99,7 +101,7 @@ let intern_ltac_variable ist = function
   | Ident (loc,id) ->
       if find_var id ist then
 	(* A local variable of any type *)
-	ArgVar (loc,id)
+        ArgVar CAst.(make ?loc id)
       else raise Not_found
   | _ ->
       raise Not_found
@@ -249,7 +251,7 @@ and intern_or_and_intro_pattern lf ist = function
       IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll)
 
 let intern_or_and_intro_pattern_loc lf ist = function
-  | ArgVar (_,id) as x ->
+  | ArgVar {v=id} as x ->
       if find_var id ist then x
       else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
   | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
@@ -261,18 +263,18 @@ let intern_intro_pattern_naming_loc lf ist (loc,pat) =
 let intern_destruction_arg ist = function
   | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c)
   | clear,ElimOnAnonHyp n as x -> x
-  | clear,ElimOnIdent (loc,id) ->
+  | clear,ElimOnIdent {loc;v=id} ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
 	let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
 	match DAst.get c with
-	| GVar id -> clear,ElimOnIdent (c.CAst.loc,id)
+        | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id)
 	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
       else
-	clear,ElimOnIdent (loc,id)
+        clear,ElimOnIdent CAst.(make ?loc id)
 
 let short_name = function
-  | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
+  | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id)
   | _ -> None
 
 let intern_evaluable_global_reference ist r =
@@ -292,9 +294,9 @@ let intern_evaluable_reference_or_by_notation ist = function
 
 (* Globalize a reduction expression *)
 let intern_evaluable ist = function
-  | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
+  | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id)
   | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist ->
-      ArgArg (EvalVarRef id, Some (loc,id))
+      ArgArg (EvalVarRef id, Some CAst.(make ?loc id))
   | r ->
       let e = intern_evaluable_reference_or_by_notation ist r in
       let na = short_name r in
@@ -370,7 +372,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
           Inr (bound_names,(c,None),dummy_pat) in
   (l, match p with
   | Inl r -> interp_ref r
-  | Inr { CAst.v = CAppExpl((None,r,None),[]) } ->
+  | Inr { v = CAppExpl((None,r,None),[]) } ->
       (* We interpret similarly @ref and ref *)
       interp_ref (AN r)
   | Inr c ->
@@ -400,8 +402,8 @@ let intern_red_expr ist = function
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
   | Simpl (f,o) ->
-     Simpl (intern_flag ist f,
-	    Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
+    Simpl (intern_flag ist f,
+           Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
@@ -438,7 +440,7 @@ let intern_pattern ist ?(as_type=false) ltacvars = function
 let intern_constr_may_eval ist = function
   | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
   | ConstrContext (locid,c) ->
-      ConstrContext (intern_hyp ist locid,intern_constr ist c)
+    ConstrContext (intern_hyp ist locid,intern_constr ist c)
   | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
   | ConstrTerm c -> ConstrTerm (intern_constr ist c)
 
@@ -452,12 +454,12 @@ let opt_cons accu = function
 
 (* Reads the hypotheses of a "match goal" rule *)
 let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
-  | (Hyp ((_,na) as locna,mp))::tl ->
+  | (Hyp ({v=na} as locna,mp))::tl ->
       let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
       let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
       let lfun' = name_cons (opt_cons lfun ido) na in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
-  | (Def ((_,na) as locna,mv,mp))::tl ->
+  | (Def ({v=na} as locna,mv,mp))::tl ->
       let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
       let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
       let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in
@@ -467,7 +469,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
 
 (* Utilities *)
 let extract_let_names lrc =
-  let fold accu ((loc, name), _) =
+  let fold accu ({loc;v=name}, _) =
     Nameops.Name.fold_right (fun id accu ->
     if Id.Set.mem id accu then user_err ?loc
       ~hdr:"glob_tactic" (str "This variable is bound several times.")
@@ -813,7 +815,7 @@ let notation_subst bindings tac =
   let fold id c accu =
     let loc = Glob_ops.loc_of_glob_constr (fst c) in
     let c = ConstrMayEval (ConstrTerm c) in
-    ((loc, Name id), c) :: accu
+    (CAst.make ?loc @@ Name id, c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in
   (** This is theoretically not correct due to potential variable capture, but
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index e3a4d5c79..8021dc715 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -47,7 +47,7 @@ val intern_constr_with_bindings :
   glob_sign -> constr_expr * constr_expr bindings ->
   glob_constr_and_expr * glob_constr_and_expr bindings
 
-val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
+val intern_hyp : glob_sign -> lident -> lident
 
 (** Adds a globalization function for extra generic arguments *)
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index f2720954d..79b5c1622 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -9,6 +9,7 @@
 open Constrintern
 open Patternops
 open Pp
+open CAst
 open Genredexpr
 open Glob_term
 open Glob_ops
@@ -363,16 +364,16 @@ let error_ltac_variable ?loc id env v s =
    strbrk "which cannot be coerced to " ++ str s ++ str".")
 
 (* Raise Not_found if not in interpretation sign *)
-let try_interp_ltac_var coerce ist env (loc,id) =
+let try_interp_ltac_var coerce ist env {loc;v=id} =
   let v = Id.Map.find id ist.lfun in
   try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
-  with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.")
+  with Not_found -> anomaly (str "Detected '" ++ Id.print locid.v ++ str "' as ltac var at interning time.")
 
 let interp_ident ist env sigma id =
-  try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id)
+  try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (make id)
   with Not_found -> id
 
 (* Interprets an optional identifier, bound or fresh *)
@@ -381,25 +382,25 @@ let interp_name ist env sigma = function
   | Name id -> Name (interp_ident ist env sigma id)
 
 let interp_intro_pattern_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id)
+  try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id)
   with Not_found -> IntroNaming (IntroIdentifier id)
 
 let interp_intro_pattern_naming_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id)
+  try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id)
   with Not_found -> IntroIdentifier id
 
-let interp_int ist locid =
+let interp_int ist ({loc;v=id} as locid) =
   try try_interp_ltac_var coerce_to_int ist None locid
   with Not_found ->
-    user_err ?loc:(fst locid) ~hdr:"interp_int"
-     (str "Unbound variable "  ++ Id.print (snd locid) ++ str".")
+    user_err ?loc ~hdr:"interp_int"
+     (str "Unbound variable "  ++ Id.print id ++ str".")
 
 let interp_int_or_var ist = function
   | ArgVar locid -> interp_int ist locid
   | ArgArg n -> n
 
 let interp_int_or_var_as_list ist = function
-  | ArgVar (_,id as locid) ->
+  | ArgVar ({v=id} as locid) ->
       (try coerce_to_int_or_var_list (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)])
   | ArgArg n as x -> [x]
@@ -408,7 +409,7 @@ let interp_int_or_var_list ist l =
   List.flatten (List.map (interp_int_or_var_as_list ist) l)
 
 (* Interprets a bound variable (especially an existing hypothesis) *)
-let interp_hyp ist env sigma (loc,id as locid) =
+let interp_hyp ist env sigma ({loc;v=id} as locid) =
   (* Look first in lfun for a value coercible to a variable *)
   try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid
   with Not_found ->
@@ -416,7 +417,7 @@ let interp_hyp ist env sigma (loc,id as locid) =
   if is_variable env id then id
   else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id))
 
-let interp_hyp_list_as_list ist env sigma (loc,id as x) =
+let interp_hyp_list_as_list ist env sigma ({loc;v=id} as x) =
   try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
   with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x]
 
@@ -425,8 +426,8 @@ let interp_hyp_list ist env sigma l =
 
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
-  | ArgVar (loc, id) ->
-    try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id)
+  | ArgVar {loc;v=id} ->
+    try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
@@ -439,7 +440,7 @@ let try_interp_evaluable env (loc, id) =
   | _ -> error_not_evaluable (VarRef id)
 
 let interp_evaluable ist env sigma = function
-  | ArgArg (r,Some (loc,id)) ->
+  | ArgArg (r,Some {loc;v=id}) ->
     (* Maybe [id] has been introduced by Intro-like tactics *)
     begin
       try try_interp_evaluable env (loc, id)
@@ -449,8 +450,8 @@ let interp_evaluable ist env sigma = function
         | _ -> error_global_not_found ?loc (qualid_of_ident id)
     end
   | ArgArg (r,None) -> r
-  | ArgVar (loc, id) ->
-    try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id)
+  | ArgVar {loc;v=id} ->
+    try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try try_interp_evaluable env (loc, id)
       with Not_found -> error_global_not_found ?loc (qualid_of_ident id)
@@ -521,9 +522,9 @@ let default_fresh_id = Id.of_string "H"
 let interp_fresh_id ist env sigma l =
   let extract_ident ist env sigma id =
     try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
-			    ist (Some (env,sigma)) (Loc.tag id)
+                            ist (Some (env,sigma)) (make id)
     with Not_found -> id in
-  let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
+  let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in
   let avoid = match TacStore.get ist.extra f_avoid_ids with
   | None -> Id.Set.empty
   | Some l -> l
@@ -535,7 +536,7 @@ let interp_fresh_id ist env sigma l =
       let s =
 	String.concat "" (List.map (function
 	  | ArgArg s -> s
-	  | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in
+          | ArgVar {v=id} -> Id.to_string (extract_ident ist env sigma id)) l) in
       let s = if CLexer.is_keyword s then s^"0" else s in
       Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
@@ -701,7 +702,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
 
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
   let p = match a with
-  | Inl (ArgVar (loc,id)) ->
+  | Inl (ArgVar {loc;v=id}) ->
       (* This is the encoding of an ltac var supposed to be bound
          prioritary to an evaluable reference and otherwise to a constr
          (it is an encoding to satisfy the "union" type given to Simpl) *)
@@ -710,7 +711,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
       with CannotCoerceTo _ ->
         let c = coerce_to_closed_constr env x in
         Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
-    (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
+    (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
      with Not_found ->
        error_global_not_found ?loc (qualid_of_ident id))
   | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
@@ -756,7 +757,7 @@ let interp_may_eval f ist env sigma = function
       let (sigma,c_interp) = f ist env sigma c in
       let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
       redfun env sigma c_interp
-  | ConstrContext ((loc,s),c) ->
+  | ConstrContext ({loc;v=s},c) ->
       (try
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
@@ -821,7 +822,7 @@ let message_of_value v =
 let interp_message_token ist = function
   | MsgString s -> Ftactic.return (str s)
   | MsgInt n -> Ftactic.return (int n)
-  | MsgIdent (loc,id) ->
+  | MsgIdent {loc;v=id} ->
     let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
     match v with
     | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
@@ -881,7 +882,7 @@ let interp_intro_pattern_naming_option ist env sigma = function
 
 let interp_or_and_intro_pattern_option ist env sigma = function
   | None -> sigma, None
-  | Some (ArgVar (loc,id)) ->
+  | Some (ArgVar {loc;v=id}) ->
       (match interp_intro_pattern_var loc ist env sigma id with
       | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
       | _ ->
@@ -906,14 +907,14 @@ let interp_binding_name ist env sigma = function
       (* If a name is bound, it has to be a quantified hypothesis *)
       (* user has to use other names for variables if these ones clash with *)
       (* a name intented to be used as a (non-variable) identifier *)
-      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id)
+      try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
 let interp_declared_or_quantified_hypothesis ist env sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var
-	    (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id)
+            (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
 let interp_binding ist env sigma (loc,(b,c)) =
@@ -924,7 +925,7 @@ let interp_bindings ist env sigma = function
 | NoBindings ->
     sigma, NoBindings
 | ImplicitBindings l ->
-    let sigma, l = interp_open_constr_list ist env sigma l in   
+    let sigma, l = interp_open_constr_list ist env sigma l in
     sigma, ImplicitBindings l
 | ExplicitBindings l ->
     let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in
@@ -959,14 +960,14 @@ let interp_destruction_arg ist gl arg =
         interp_open_constr_with_bindings ist env sigma c
       end
   | keep,ElimOnAnonHyp n as x -> x
-  | keep,ElimOnIdent (loc,id) ->
+  | keep,ElimOnIdent {loc;v=id} ->
       let error () = user_err ?loc 
        (strbrk "Cannot coerce " ++ Id.print id ++
         strbrk " neither to a quantified hypothesis nor to a term.")
       in
       let try_cast_id id' =
         if Tactics.is_quantified_hypothesis id' gl
-        then keep,ElimOnIdent (loc,id')
+        then keep,ElimOnIdent CAst.(make ?loc id')
         else
           (keep, ElimOnConstr begin fun env sigma ->
           try (sigma, (constr_of_id env id', NoBindings))
@@ -994,7 +995,7 @@ let interp_destruction_arg ist gl arg =
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
-          keep,ElimOnIdent (loc,id)
+          keep,ElimOnIdent CAst.(make ?loc id)
 	else
           let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
           let f env sigma =
@@ -1043,11 +1044,11 @@ let cons_and_check_name id l =
   else id::l
 
 let rec read_match_goal_hyps lfun ist env sigma lidh = function
-  | (Hyp ((loc,na) as locna,mp))::tl ->
+  | (Hyp ({loc;v=na} as locna,mp))::tl ->
       let lidh' = Name.fold_right cons_and_check_name na lidh in
       Hyp (locna,read_pattern lfun ist env sigma mp)::
 	(read_match_goal_hyps lfun ist env sigma lidh' tl)
-  | (Def ((loc,na) as locna,mv,mp))::tl ->
+  | (Def ({loc;v=na} as locna,mv,mp))::tl ->
       let lidh' = Name.fold_right cons_and_check_name na lidh in
       Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp)::
 	(read_match_goal_hyps lfun ist env sigma lidh' tl)
@@ -1112,7 +1113,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
         in
 	Tactic_debug.debug_prompt lev tac eval
   | _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-      
+
 
 and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacAtom (loc,t) ->
@@ -1248,7 +1249,7 @@ and force_vrec ist v : Val.t Ftactic.t =
 
 and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
   match r with
-  | ArgVar (loc,id) ->
+  | ArgVar {loc;v=id} ->
       let v =
         try Id.Map.find id ist.lfun
         with Not_found -> in_gen (topwit wit_var) id
@@ -1416,7 +1417,7 @@ and tactic_of_value ist vle =
 and interp_letrec ist llc u =
   Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
-  let fold accu ((_, na), b) =
+  let fold accu ({v=na}, b) =
     let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
     Name.fold_right (fun id -> Id.Map.add id v) na accu
   in
@@ -1431,7 +1432,7 @@ and interp_letin ist llc u =
   | [] ->
     let ist = { ist with lfun } in
     val_interp ist u
-  | ((_, na), body) :: defs ->
+  | ({v=na}, body) :: defs ->
     Ftactic.bind (interp_tacarg ist body) (fun v ->
     fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs)
   in
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 5f2723a1e..2d448e832 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -75,7 +75,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
 (** Interprets tactic expressions *)
 
 val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map ->
-  Id.t Loc.located -> Id.t
+  lident -> Id.t
 
 val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map ->
   ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr ->
@@ -125,9 +125,9 @@ val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> uni
 (** Internals that can be useful for syntax extensions. *)
 
 val interp_ltac_var : (value -> 'a) -> interp_sign ->
-  (Environ.env * Evd.evar_map) option -> Id.t Loc.located -> 'a
+  (Environ.env * Evd.evar_map) option -> lident -> 'a
 
-val interp_int : interp_sign -> Id.t Loc.located -> int
+val interp_int : interp_sign -> lident -> int
 
 val interp_int_or_var : interp_sign -> int or_var -> int
 
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 2475e41f9..dce6f5558 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -74,7 +74,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
-  Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
+  Misctypes.lident message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
   ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index e87951dd7..6bf9215e0 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -306,9 +306,9 @@ module PatternMatching (E:StaticEnvironment) = struct
       [pat] is [Hyp _] or [Def _]. *)
   let hyp_match pat hyps =
     match pat with
-    | Hyp ((_,hypname),typepat) ->
+    | Hyp ({CAst.v=hypname},typepat) ->
         hyp_match_type hypname typepat hyps
-    | Def ((_,hypname),bodypat,typepat) ->
+    | Def ({CAst.v=hypname},bodypat,typepat) ->
         hyp_match_body_and_type hypname bodypat typepat hyps
 
   (** [hyp_pattern_list_match pats hyps lhs], matches the list of
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 01d3f79c7..5ce30c3d7 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -255,10 +255,10 @@ let tauto_power_flags = {
 }
 
 let with_flags flags _ ist =
-  let f = (Loc.tag @@ Id.of_string "f") in
-  let x = (Loc.tag @@ Id.of_string "x") in
+  let f = CAst.make @@ Id.of_string "f" in
+  let x = CAst.make @@ Id.of_string "x" in
   let arg = Val.Dyn (tag_tauto_flags, flags) in
-  let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in
+  let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
   eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)]))))
 
 let register_tauto_tactic tac name0 args =