[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.

26 files changed, 250 insertions, 231 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 693ab464d..22881c32c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1295,7 +1295,7 @@ let rec rebuild_return_type rt =
         CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
 	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous],
+    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
                                        Constrexpr.Default Decl_kinds.Explicit, rt)],
 			    CAst.make @@ Constrexpr.CSort(GType []))
 
@@ -1351,12 +1351,12 @@ let do_build_inductive
 	(fun (n,t,typ) acc ->
           match typ with
           | Some typ ->
-	     CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+             CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
 	  | None ->
 	     CAst.make @@ Constrexpr.CProdN
-               ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
+               ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
 		acc
 	       )
 	)
@@ -1418,12 +1418,12 @@ let do_build_inductive
       (fun (n,t,typ) acc ->
          match typ with
          | Some typ ->
-	   CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+           CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
 	 | None ->
            CAst.make @@ Constrexpr.CProdN
-           ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
+           ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
 	    acc
 	   )
       )
@@ -1450,18 +1450,18 @@ let do_build_inductive
       (fun (n,t,typ) ->
          match typ with
          | Some typ ->
-	   Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t,
+           Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t,
                                   Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ))
 	 | None ->
 	 Constrexpr.CLocalAssum
-	   ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
+           ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
   in
   let ext_rels_constructors =
     Array.map (List.map
       (fun (id,t) ->
-	 false,((Loc.tag id),
+         false,((CAst.make id),
 		with_full_print
 		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t))
 	       )
@@ -1469,7 +1469,7 @@ let do_build_inductive
       (rel_constructors)
   in
   let rel_ind i ext_rel_constructors =
-    (((Loc.tag @@ relnames.(i)), None),
+    (((CAst.make @@ relnames.(i)), None),
     rel_params,
     Some rel_arities.(i),
     ext_rel_constructors),[]
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 96e4a94d3..e19fc9b62 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -155,7 +155,7 @@ let build_newrecursive
   let sigma = Evd.from_env env0 in
   let (rec_sign,rec_impls) =
     List.fold_left
-      (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
+      (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) ->
         let arityc = Constrexpr_ops.mkCProdN bl arityc in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
         let evd = Evd.from_env env0 in
@@ -344,7 +344,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
     (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
       Tacmach.tactic) : unit =
-  let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
+  let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
   let funs_types =  List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in
@@ -365,7 +365,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 		 f_R_mut)
 	in
 	let fname_kn (((fname,_),_,_,_,_),_) =
-	  let f_ref = Ident fname in
+          let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in
 	  locate_with_msg
 	    (pr_reference f_ref++str ": Not an inductive type!")
 	    locate_constant
@@ -404,7 +404,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
-    | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
+    | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
       ComDefinition.do_definition
         ~program_mode:false
@@ -413,7 +413,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
-	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+           (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -430,7 +430,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
-	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
+           (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
@@ -460,7 +460,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   let rec_arg_num =
     let names =
       List.map
-	snd
+        CAst.(with_val (fun x -> x))
 	(Constrexpr_ops.names_of_local_assums args)
     in
     match wf_arg with
@@ -476,8 +476,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 (None,(Ident (Loc.tag fname)),None) ,
 	 (List.map
 	    (function
-	       | _,Anonymous -> assert false
-	       | _,Name e -> (Constrexpr_ops.mkIdentC e)
+               | {CAst.v=Anonymous} -> assert false
+               | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e)
 	    )
 	    (Constrexpr_ops.names_of_local_assums args)
 	 )
@@ -515,7 +515,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
       | None ->
 	  begin
 	    match args with
-	      | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x
+              | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x
 	      | _ -> error "Recursive argument must be specified"
 	  end
       | Some wf_args ->
@@ -525,7 +525,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 		(function
 		   | Constrexpr.CLocalAssum(l,k,t) ->
 		       List.exists
-			 (function (_,Name id) -> Id.equal id wf_args | _ -> false)
+                         (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false)
 			 l
 		   | _ -> false
 		)
@@ -546,7 +546,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	  let fun_from_mes =
 	    let applied_mes =
 	      Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg])    in
-	    Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
+            Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes)
 	  in
 	  let wf_rel_from_mes =
 	    Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC  ltof,[wf_arg_type;fun_from_mes])
@@ -557,7 +557,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    let a = Names.Id.of_string "___a" in 
 	    let b = Names.Id.of_string "___b" in 
 	    Constrexpr_ops.mkLambdaC(
-	      [Loc.tag @@ Name a;Loc.tag @@ Name b],
+              [CAst.make @@ Name a; CAst.make @@ Name b],
 	      Constrexpr.Default Explicit,
 	      wf_arg_type,
 	      Constrexpr_ops.mkAppC(wf_rel_expr,
@@ -592,7 +592,7 @@ and rebuild_nal aux bk bl' nal typ =
 	  | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
 	  | [], _ -> rebuild_bl aux bl' typ
           | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } ->
-	     if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
+             if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v)
 	     then
 	       let assum = CLocalAssum([na],bk,nal't) in
                let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
@@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   let _is_struct =
     match fixpoint_exprl with
       | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
- 	  let (((((_,name),pl),_,args,types,body)),_)  as fixpoint_expr =
+          let (((({CAst.v=name},pl),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
 	      | _ -> assert false
@@ -659,10 +659,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-	  then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook;
+          then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
 	  false
       |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] ->
- 	  let (((((_,name),_),_,args,types,body)),_)  as fixpoint_expr =
+          let (((({CAst.v=name},_),_,args,types,body)),_)  as fixpoint_expr =
 	    match recompute_binder_list [fixpoint_expr] with 
 	      | [e] -> e
 	      | _ -> assert false
@@ -683,7 +683,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      true
 	  in
 	  if register_built
-	  then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook;
+          then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook;
 	  true
       | _ ->
 	  List.iter (function ((_na,(_,ord),_args,_body,_type),_not) ->
@@ -696,7 +696,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	    fixpoint_exprl;
 	let fixpoint_exprl = recompute_binder_list fixpoint_exprl in 
 	let fix_names =
-	  List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl
+          List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl
 	in
 	(* ok all the expressions are structural *)
   	let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
@@ -757,7 +757,7 @@ let rec add_args id new_args = CAst.map (function
 	     List.map (fun (b,na,b_option) ->
 			 add_args id new_args b,
 			 na, b_option) cel,
-	     List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal
+             List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal
 	    )
   | CLetTuple(nal,(na,b_option),b1,b2) ->
       CLetTuple(nal,(na,Option.map (add_args id new_args) b_option),
@@ -875,7 +875,7 @@ let make_graph (f_ref:global_reference) =
 		 let l =
 		   List.map
 		     (fun (id,(n,recexp),bl,t,b) ->
-			let loc, rec_id = Option.get n in
+                        let { CAst.loc; v=rec_id } = Option.get n in
 			let new_args =
 			  List.flatten
 			    (List.map
@@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalDef (na,_,_)-> []
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
-					(fun (loc,n) -> CAst.make ?loc @@ 
+                                        (fun {CAst.loc;v=n} -> CAst.make ?loc @@
 					   CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
@@ -891,21 +891,21 @@ let make_graph (f_ref:global_reference) =
 			       nal_tas
 			    )
 			in
-			let b' = add_args (snd id) new_args b in
-			((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
+                        let b' = add_args id.CAst.v new_args b in
+                        ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
 		     )
 		     fixexprl
 		 in
 		 l
 	     | _ ->
 		let id = Label.to_id (Constant.label c) in
-		 [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
+                 [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 let mp,dp,_ = Constant.repr3 c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
-	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
+           (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
 	   expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true
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 =
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 40897d62f..55dc7f580 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -22,7 +22,7 @@ let x = Id.of_string "x"
 
 let make_cont (k : Val.t) (c : EConstr.t) =
   let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (Loc.tag (ArgVar (Loc.tag cont), [Reference (ArgVar (Loc.tag x))])) in
+  let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
   Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e3e749b75..125afb1a0 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -166,12 +166,12 @@ let ltac_call tac (args:glob_tactic_arg list) =
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args)))
+  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args)))
 
 let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
   let fold arg (i, vars, lfun) =
     let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar (Loc.tag id)) in
+    let x = Reference (ArgVar CAst.(make id)) in
     (succ i, x :: vars, Id.Map.add id arg lfun)
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
@@ -206,7 +206,7 @@ let get_res =
 let exec_tactic env evd n f args =
   let fold arg (i, vars, lfun) =
     let id = Id.of_string ("x" ^ string_of_int i) in
-    let x = Reference (ArgVar (Loc.tag id)) in
+    let x = Reference (ArgVar CAst.(make id)) in
     (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun)
   in
   let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 499154d50..4ae746288 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -268,7 +268,7 @@ let interp_wit wit ist gl x =
   sigma, Tacinterp.Value.cast (topwit wit) arg
 
 let interp_hyp ist gl (SsrHyp (loc, id)) =
-  let s, id' = interp_wit wit_var ist gl (loc, id) in
+  let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in
   if not_section_id id' then s, SsrHyp (loc, id') else
   hyp_err ?loc "Can't clear section hypothesis " id'
 
@@ -835,9 +835,9 @@ let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
 let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t =  CAst.make ?loc @@
-   CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t)
+   CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
-   CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t)
+   CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty)
 
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
@@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    | _, (_, Some ty) ->
     let rec force_type ty = CAst.(map (function
      | CProdN (abs, t) ->
-       n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs));
+       n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs));
        CProdN (abs, force_type t)
      | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 211cad3f5..0d8044f19 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -130,7 +130,7 @@ let pr_ssrhyp _ _ _ = pr_hyp
 let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp
 
 let intern_hyp ist (SsrHyp (loc, id) as hyp) =
-  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in
+  let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in
   if not_section_id id then hyp else
   hyp_err ?loc "Can't clear section hypothesis " id
 
@@ -316,7 +316,7 @@ END
 
 
 let pr_index = function
-  | Misctypes.ArgVar (_, id) -> pr_id id
+  | Misctypes.ArgVar {CAst.v=id} -> pr_id id
   | Misctypes.ArgArg n when n > 0 -> int n
   | _ -> mt ()
 let pr_ssrindex _ _ _ = pr_index
@@ -330,13 +330,13 @@ let mk_index ?loc = function
   | iv -> iv
 
 let interp_index ist gl idx =
-  Tacmach.project gl, 
+  Tacmach.project gl,
   match idx with
   | Misctypes.ArgArg _ -> idx
-  | Misctypes.ArgVar (loc, id) ->
+  | Misctypes.ArgVar id ->
     let i =
       try
-        let v = Id.Map.find id ist.Tacinterp.lfun in
+        let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
         begin match Tacinterp.Value.to_int v with
         | Some i -> i
         | None ->
@@ -350,8 +350,8 @@ let interp_index ist gl idx =
           end
         | None -> raise Not_found
         end end
-    with _ -> CErrors.user_err ?loc (str"Index not a number") in
-    Misctypes.ArgArg (check_index ?loc i)
+    with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
+    Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
 
 open Pltac
 
@@ -1014,22 +1014,22 @@ let rec mkBstruct i = function
   | [] -> []
 
 let rec format_local_binders h0 bl0 = match h0, bl0 with
-  | BFvar :: h, CLocalAssum ([_, x], _,  _) :: bl ->
+  | BFvar :: h, CLocalAssum ([{CAst.v=x}], _,  _) :: bl ->
     Bvar x :: format_local_binders h bl
   | BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl ->
-    Bdecl (List.map snd lxs, t) :: format_local_binders h bl
-  | BFdef :: h, CLocalDef ((_, x), v, oty) :: bl ->
+    Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl
+  | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl ->
     Bdef (x, oty, v) :: format_local_binders h bl
   | _ -> []
   
 let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
-  | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } ->
+  | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } ->
     let bs, c' = format_constr_expr h c in
     Bvar x :: bs, c'
   | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } ->
     let bs, c' = format_constr_expr h c in
-    Bdecl (List.map snd lxs, t) :: bs, c'
-  | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } ->
+    Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c'
+  | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
   | [BFcast], { v = CCast (c, CastConv t) } ->
@@ -1037,7 +1037,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFrec (has_str, has_cast) :: h, 
     { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
     let bs = format_local_binders h bl in
-    let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in
+    let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in
     bs @ bstr @ (if has_cast then [Bcast t] else []), c 
   | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } ->
     format_local_binders h bl @ (if has_cast then [Bcast t] else []), c
@@ -1156,18 +1156,18 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar
 END
 
 let bvar_lname = let open CAst in function
-  | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id
-  | { loc = loc } -> Loc.tag ?loc Anonymous
+  | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id
+  | { loc = loc } -> CAst.make ?loc Anonymous
 
 let pr_ssrbinder prc _ _ (_, c) = prc c
 
 ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder
  | [ ssrbvar(bv) ] ->
-   [ let xloc, _ as x = bvar_lname bv in
+   [ let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
      CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ")" ] ->
-   [ let xloc, _ as x = bvar_lname bv in
+   [ let { CAst.loc=xloc } as x = bvar_lname bv in
      (FwdPose, [BFvar]),
      CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
@@ -1191,7 +1191,7 @@ GEXTEND Gram
   [  ["of" | "&"]; c = operconstr LEVEL "99" ->
      let loc = !@loc in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
   ];
 END
 
@@ -1250,13 +1250,13 @@ END
 let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd
 
 let bvar_locid = function
-  | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id
+  | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id
   | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"")
 
 
 ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
   | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] ->
-    [ let (_, id) as lid = bvar_locid bv in
+    [ let { CAst.v=id } as lid = bvar_locid bv in
       let (fk, h), (ck, (rc, oc)) = fwd in
       let c = Option.get oc in
       let has_cast, t', c' = match format_constr_expr h c with
@@ -1265,8 +1265,10 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd
       let lb = fix_binders bs in
       let has_struct, i =
         let rec loop = function
-          (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id')
-          | [l', Name id'] when sid = None -> false, (l', id')
+          | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') ->
+            true, CAst.make ?loc:l' id'
+          | [{CAst.loc=l';v=Name id'}] when sid = None ->
+            false, CAst.make ?loc:l' id'
           | _ :: bn -> loop bn
           | [] -> CErrors.user_err (Pp.str "Bad structural argument") in
         loop (names_of_local_assums lb) in
@@ -1282,7 +1284,7 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd
 
 ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd
   | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] ->
-    [ let _, id as lid = bvar_locid bv in
+    [ let { CAst.v=id } as lid = bvar_locid bv in
       let (fk, h), (ck, (rc, oc)) = fwd in
       let c = Option.get oc in
       let has_cast, t', c' = match format_constr_expr h c with
@@ -1323,7 +1325,7 @@ END
 
 let intro_id_to_binder = List.map (function 
   | IPatId id ->
-      let xloc, _ as x = bvar_lname (mkCVar id) in
+      let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
         CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
           mkCHole None)
@@ -1332,9 +1334,9 @@ let intro_id_to_binder = List.map (function
 let binder_to_intro_id = CAst.(List.map (function
   | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
   | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
-      List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids
-  | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id]
-  | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One]
+      List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids
+  | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id]
+  | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One]
   | _ -> anomaly "ssrbinder is not a binder"))
 
 let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) =
@@ -1405,7 +1407,7 @@ let ssrorelse = Gram.entry_create "ssrorelse"
 GEXTEND Gram
   GLOBAL: ssrorelse ssrseqarg;
   ssrseqidx: [
-    [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id)
+    [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id)
     | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n)
     ] ];
   ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]];
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 25d1472f1..8e6e0347f 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -79,9 +79,9 @@ let aliasvar = function
 let mk_cnotype mp = aliasvar mp, None in
 let mk_ctype mp t = aliasvar mp, Some t in
 let mk_rtype t = Some t in
-let mk_dthen ?loc (mp, ct, rt) c = (Loc.tag ?loc (mp, c)), ct, rt in
+let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt in
 let mk_let ?loc rt ct mp c1 =
-  CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [Loc.tag ?loc (mp, c1)]) in
+  CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) in
 let mk_pat c (na, t) = (c, na, t) in
 GEXTEND Gram
   GLOBAL: binder_constr;
@@ -94,14 +94,16 @@ GEXTEND Gram
   ] ];
   ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]];
   ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]];
-  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]];
+  ssr_else: [[ mp = ssr_elsepat; c = lconstr -> CAst.make ~loc:!@loc (mp, c) ]];
   binder_constr: [
     [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else ->
       let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2])
     | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else ->
       let b1, ct, rt = db1 in 
-      let b1, b2 = 
-        let (l1, (p1, r1)), (l2, (p2, r2)) = b1, b2 in (l1, (p1, r2)), (l2, (p2, r1)) in
+      let b1, b2 = let open CAst in
+        let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in
+        (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1))
+      in
       CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2])
     | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr ->
       mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1
@@ -118,7 +120,7 @@ GEXTEND Gram
   GLOBAL: closed_binder;
   closed_binder: [
     [ ["of" | "&"]; c = operconstr LEVEL "99" ->
-      [CLocalAssum ([Loc.tag ~loc:!@loc Anonymous], Default Explicit, c)]
+      [CLocalAssum ([CAst.make ~loc:!@loc Anonymous], Default Explicit, c)]
   ] ];
 END
 (* }}} *)
@@ -553,7 +555,7 @@ GEXTEND Gram
           let s = coerce_reference_to_id qid in
     Vernacexpr.VernacDefinition
       ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure),
-          ((Loc.tag (Name s)),None), d)
+          ((CAst.make (Name s)),None), d)
   ]];
 END
 
@@ -584,10 +586,10 @@ END
 GEXTEND Gram
   GLOBAL: hloc;
 hloc: [
-  [ "in"; "("; "Type"; "of"; id = ident; ")" -> 
-    Tacexpr.HypLocation ((Loc.tag id), Locus.InHypTypeOnly)
-  | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> 
-    Tacexpr.HypLocation ((Loc.tag id), Locus.InHypValueOnly)
+  [ "in"; "("; "Type"; "of"; id = ident; ")" ->
+    Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly)
+  | "in"; "("; IDENT "Value"; "of"; id = ident; ")" ->
+    Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly)
   ] ];
 END
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 71e8b4ac4..73e212365 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -137,9 +137,9 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
 let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
 let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t = CAst.make ?loc @@
-   CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t)
+   CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
 let mkCLetIn ?loc name bo t = CAst.make ?loc @@
-   CLetIn ((Loc.tag ?loc name), bo, None, t)
+   CLetIn ((CAst.make ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
 let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)