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

15 files changed, 203 insertions, 206 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8aca6e333..d05e7d909 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -61,13 +61,13 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
   Id.equal id1 id2
 | _ -> false
 
-let eq_located f (_, x) (_, y) = f x y
+let eq_ast f { CAst.v = x } { CAst.v = y } = f x y
 
 let rec cases_pattern_expr_eq p1 p2 =
   if CAst.(p1.v == p2.v) then true
   else match CAst.(p1.v, p2.v) with
   | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
-      Name.equal (snd i1) (snd i2) && cases_pattern_expr_eq a1 a2
+      eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
       eq_reference c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
@@ -106,10 +106,10 @@ let rec constr_expr_eq e1 e2 =
   else match CAst.(e1.v, e2.v) with
     | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
     | CFix(id1,fl1), CFix(id2,fl2) ->
-      eq_located Id.equal id1 id2 &&
+      eq_ast Id.equal id1 id2 &&
       List.equal fix_expr_eq fl1 fl2
     | CCoFix(id1,fl1), CCoFix(id2,fl2) ->
-      eq_located Id.equal id1 id2 &&
+      eq_ast Id.equal id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
     | CProdN(bl1,a1), CProdN(bl2,a2) ->
       List.equal local_binder_eq bl1 bl2 &&
@@ -117,8 +117,8 @@ let rec constr_expr_eq e1 e2 =
     | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
       List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
-    | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
-      Name.equal na1 na2 &&
+    | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) ->
+      eq_ast Name.equal na1 na2 &&
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
@@ -141,14 +141,14 @@ let rec constr_expr_eq e1 e2 =
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
     | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
-      List.equal (eq_located Name.equal) n1 n2 &&
-      Option.equal (eq_located Name.equal) m1 m2 &&
+      List.equal (eq_ast Name.equal) n1 n2 &&
+      Option.equal (eq_ast Name.equal) m1 m2 &&
       Option.equal constr_expr_eq e1 e2 &&
       constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
     | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
       constr_expr_eq e1 e2 &&
-      Option.equal (eq_located Name.equal) n1 n2 &&
+      Option.equal (eq_ast Name.equal) n1 n2 &&
       Option.equal constr_expr_eq r1 r2 &&
       constr_expr_eq t1 t2 &&
       constr_expr_eq f1 f2
@@ -181,28 +181,28 @@ let rec constr_expr_eq e1 e2 =
      | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
-  Option.equal (eq_located explicitation_eq) e1 e2 &&
+  Option.equal (eq_ast explicitation_eq) e1 e2 &&
   constr_expr_eq a1 a2
 
 and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   constr_expr_eq e1 e2 &&
-  Option.equal (eq_located Name.equal) n1 n2 &&
+  Option.equal (eq_ast Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
 
-and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
+and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
   List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
-  (eq_located Id.equal id1 id2) &&
-  Option.equal (eq_located Id.equal) j1 j2 &&
+  (eq_ast Id.equal id1 id2) &&
+  Option.equal (eq_ast Id.equal) j1 j2 &&
   recursion_order_expr_eq r1 r2 &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
 
 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
-  (eq_located Id.equal id1 id2) &&
+  (eq_ast Id.equal id1 id2) &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
@@ -216,10 +216,10 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
 
 and local_binder_eq l1 l2 = match l1, l2 with
   | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
-    eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
+    eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
   | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
     (** Don't care about the [binder_kind] *)
-    List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
+    List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
   | _ -> false
 
 and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
@@ -244,12 +244,12 @@ and cast_expr_eq c1 c2 = match c1, c2 with
 let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
-let local_binder_loc = function
-  | CLocalAssum ((loc,_)::_,_,t)
-  | CLocalDef ((loc,_),t,None) -> Loc.merge_opt loc (constr_loc t)
-  | CLocalDef ((loc,_),b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
+let local_binder_loc = let open CAst in function
+  | CLocalAssum ({ loc } ::_,_,t)
+  | CLocalDef ( { loc },t,None) -> Loc.merge_opt loc (constr_loc t)
+  | CLocalDef ( { loc },b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
   | CLocalAssum ([],_,_) -> assert false
-  | CLocalPattern (loc,_) -> loc
+  | CLocalPattern { loc } -> loc
 
 let local_binders_loc bll = match bll with
   | []     -> None
@@ -257,9 +257,6 @@ let local_binders_loc bll = match bll with
 
 (** Folds and maps *)
 
-(* Legacy functions *)
-let down_located f (_l, x) = f x
-
 let is_constructor id =
   try Globnames.isConstructRef
         (Smartlocate.global_of_extended_global
@@ -269,7 +266,7 @@ let is_constructor id =
 let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
   | CPatRecord l ->
     List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
-  | CPatAlias (pat,(loc,na)) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
+  | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
   | CPatOr (patl) ->
     List.fold_left (cases_pattern_fold_names f) a patl
   | CPatCstr (_,patl1,patl2) ->
@@ -301,17 +298,17 @@ let ids_of_cases_tomatch tms =
     (fun (_, ona, indnal) l ->
        Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
          indnal
-         (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
+         (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
-let rec fold_local_binders g f n acc b = function
+let rec fold_local_binders g f n acc b = let open CAst in function
   | CLocalAssum (nal,bk,t)::l ->
-    let nal = snd (List.split nal) in
+    let nal = List.(map (fun {v} -> v) nal) in
     let n' = List.fold_right (Name.fold_right g) nal n in
     f n (fold_local_binders g f n' acc b l) t
-  | CLocalDef ((_,na),c,t)::l ->
+  | CLocalDef ( { v = na },c,t)::l ->
     Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
-  | CLocalPattern (_,(pat,t))::l ->
+  | CLocalPattern { v = pat,t }::l ->
     let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
     Option.fold_left (f n) acc t
   | [] ->
@@ -322,7 +319,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
     | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
     | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
-      f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+      f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
     | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
     | CCast (a,CastCoerce) -> f n acc a
     | CNotation (_,(l,ll,bl,bll)) ->
@@ -339,18 +336,18 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
-      List.fold_right (fun (loc,(patl,rhs)) acc ->
+      List.fold_right (fun {CAst.v=(patl,rhs)} acc ->
           let ids = ids_of_pattern_list patl in
           f (Id.Set.fold g ids n) acc rhs) bl acc
     | CLetTuple (nal,(ona,po),b,c) ->
-      let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
-      f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
+      let n' = List.fold_right (CAst.with_val (Name.fold_right g)) nal n in
+      f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n') (f n acc b) c
     | CIf (c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
-        (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po
+        (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
     | CFix (_,l) ->
-      let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
+      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
           fold_local_binders g f n'
             (fold_local_binders g f n acc t lb) c lb) l acc
@@ -369,18 +366,19 @@ let free_vars_of_constr_expr c =
 let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 
 (* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
+let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e
 
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+  let open CAst in
   let h (e,bl) = function
       CLocalAssum(nal,k,ty) ->
       (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
-    | CLocalDef((loc,na),c,ty) ->
-      (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
-    | CLocalPattern (loc,(pat,t)) ->
+    | CLocalDef( { loc ; v = na } as cna ,c,ty) ->
+      (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
+    | CLocalPattern { loc; v = pat,t } ->
       let ids = ids_of_pattern pat in
-      (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
+      (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
@@ -393,7 +391,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CLambdaN (bl,b) ->
       let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
     | CLetIn (na,a,t,b) ->
-      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
+      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
     | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
     | CNotation (n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
@@ -405,32 +403,32 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CPrim _ | CRef _ as x -> x
     | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l)
     | CCases (sty,rtnpo,a,bl) ->
-      let bl = List.map (fun (loc,(patl,rhs)) ->
+      let bl = List.map (fun {CAst.v=(patl,rhs);loc} ->
           let ids = ids_of_pattern_list patl in
-          (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in
+          CAst.make ?loc (patl,f (Id.Set.fold g ids e) rhs)) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
     | CLetTuple (nal,(ona,po),b,c) ->
-      let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
-      let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
+      let e' = List.fold_right (CAst.with_val (Name.fold_right g)) nal e in
+      let e'' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
       CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
     | CIf (c,(ona,po),b1,b2) ->
-      let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
+      let e' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
     | CFix (id,dl) ->
       CFix (id,List.map (fun (id,n,bl,t,d) ->
           let (e',bl') = map_local_binders f g e bl in
           let t' = f e' t in
           (* Note: fix names should be inserted before the arguments... *)
-          let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,n,bl',t',d')) dl)
     | CCoFix (id,dl) ->
       CCoFix (id,List.map (fun (id,bl,t,d) ->
           let (e',bl') = map_local_binders f g e bl in
           let t' = f e' t in
-          let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,bl',t',d')) dl)
     | CProj (p,c) ->
@@ -471,17 +469,18 @@ let error_invalid_pattern_notation ?loc () =
 
 (* Interpret the index of a recursion order annotation *)
 let split_at_annot bl na =
-  let names = List.map snd (names_of_local_assums bl) in
+  let open CAst in
+  let names = List.map (fun { v } -> v) (names_of_local_assums bl) in
   match na with
   | None ->
     begin match names with
       | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.")
       | _ -> ([], bl)
     end
-  | Some (loc, id) ->
+  | Some { loc; v = id } ->
     let rec aux acc = function
       | CLocalAssum (bls, k, t) as x :: rest ->
-        let test (_, na) = match na with
+        let test { CAst.v = na } = match na with
           | Name id' -> Id.equal id id'
           | Anonymous -> false
         in
@@ -495,13 +494,13 @@ let split_at_annot bl na =
             in
             (List.rev ans, CLocalAssum (r, k, t) :: rest)
         end
-      | CLocalDef ((_,na),_,_) as x :: rest ->
+      | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
         if Name.equal (Name id) na then
           CErrors.user_err ?loc
             (Id.print id ++ str" must be a proper parameter and not a local definition.")
         else
           aux (x :: acc) rest
-      | CLocalPattern (_,_) :: rest ->
+      | CLocalPattern _ :: rest ->
         Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
       | [] ->
         CErrors.user_err ?loc
@@ -536,14 +535,14 @@ let coerce_reference_to_id = function
       (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
-  | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id)
+  | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc id
   | { CAst.loc; _ } -> CErrors.user_err ?loc
                          ~hdr:"coerce_to_id"
                          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
-  | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id)
-  | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous)
+  | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc @@ Name id
+  | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
 
@@ -569,8 +568,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
      CPatAtom (Some r)
   | CHole (None,Misctypes.IntroAnonymous,None) ->
      CPatAtom None
-  | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
-      CPatAlias (coerce_to_cases_pattern_expr b, (loc,Name id))
+  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
+      CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
   | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
      (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
   | CAppExpl ((None,r,i),args) ->
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 0b00b0e4d..50c818d3c 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Libnames
 open Misctypes
@@ -44,9 +43,9 @@ val mkIdentC : Id.t -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
 val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
-val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
-val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
+val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
+val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
 
 val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
 (** Same as [abstract_constr_expr], with location *)
@@ -72,10 +71,10 @@ val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr
 val coerce_reference_to_id : reference -> Id.t
 (** FIXME: nothing to do here *)
 
-val coerce_to_id : constr_expr -> Id.t located
+val coerce_to_id : constr_expr -> lident
 (** Destruct terms of the form [CRef (Ident _)]. *)
 
-val coerce_to_name : constr_expr -> Name.t located
+val coerce_to_name : constr_expr -> lname
 (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *)
 
 val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
@@ -84,10 +83,10 @@ val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr
 
 val default_binder_kind : binder_kind
 
-val names_of_local_binders : local_binder_expr list -> Name.t located list
+val names_of_local_binders : local_binder_expr list -> lname list
 (** Retrieve a list of binding names from a list of binders. *)
 
-val names_of_local_assums : local_binder_expr list -> Name.t located list
+val names_of_local_assums : local_binder_expr list -> lname list
 (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into
     account. *)
 
@@ -113,7 +112,7 @@ val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t
 val free_vars_of_constr_expr : constr_expr -> Id.Set.t
 val occur_var_constr_expr : Id.t -> constr_expr -> bool
 
-val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
+val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list
 
 val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9e18966b6..dec86ba81 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -257,7 +257,7 @@ let insert_pat_delimiters ?loc p = function
 
 let insert_pat_alias ?loc p = function
   | Anonymous -> p
-  | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(loc,na))
+  | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na))
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -574,7 +574,7 @@ let explicitize inctx impl (cf,f) args =
 	   is_significant_implicit (Lazy.force a))
 	in
         if visible then
-	  (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail
+          (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail
 	else
 	  tail
     | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
@@ -816,7 +816,7 @@ let rec extern inctx scopes vars r =
              (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
 
   | GLetIn (na,b,t,c) ->
-      CLetIn ((loc,na),sub_extern false scopes vars b,
+      CLetIn (make ?loc na,sub_extern false scopes vars b,
               Option.map (extern_typ scopes vars) t,
               extern inctx scopes (add_vname vars na) c)
 
@@ -840,12 +840,12 @@ let rec extern inctx scopes vars r =
                             | None -> None
                             | Some ntn ->
                                if occur_glob_constr id ntn then
-                                 Some (Loc.tag Anonymous)
+                                 Some (CAst.make Anonymous)
                                else None
                       end
                    | Anonymous, _ -> None
                    | Name id, GVar id' when Id.equal id id' -> None
-                   | Name _, _ -> Some (Loc.tag na) in
+                   | Name _, _ -> Some (CAst.make na) in
                  (sub_extern false scopes vars tm,
                   na',
                   Option.map (fun (loc,(ind,nal)) ->
@@ -859,15 +859,15 @@ let rec extern inctx scopes vars r =
     CCases (sty,rtntypopt',tml,eqns)
 
   | GLetTuple (nal,(na,typopt),tm,b) ->
-      CLetTuple (List.map (fun na -> (Loc.tag na)) nal,
-        (Option.map (fun _ -> (Loc.tag na)) typopt,
+    CLetTuple (List.map CAst.make nal,
+        (Option.map (fun _ -> (make na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern inctx scopes (List.fold_left add_vname vars nal) b)
 
   | GIf (c,(na,typopt),b1,b2) ->
       CIf (sub_extern false scopes vars c,
-        (Option.map (fun _ -> (Loc.tag na)) typopt,
+        (Option.map (fun _ -> (CAst.make na)) typopt,
          Option.map (extern_typ scopes (add_vname vars na)) typopt),
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
@@ -885,13 +885,13 @@ let rec extern inctx scopes vars r =
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
-		     | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x))
+                     | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
 		 in
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
-		 ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
+                 ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in
-	     CFix ((loc,idv.(n)),Array.to_list listdecl)
+             CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
 	 | GCoFix n ->
 	     let listdecl =
                Array.mapi (fun i fi ->
@@ -899,10 +899,10 @@ let rec extern inctx scopes vars r =
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
                  let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
-		 ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
+                 ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
-	     CCoFix ((loc,idv.(n)),Array.to_list listdecl))
+             CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
 
   | GSort s -> CSort (extern_glob_sort s)
 
@@ -932,7 +932,7 @@ and factorize_prod scopes vars na bk aty c =
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = extern_typ scopes vars b in
       let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
-      let binder = CLocalPattern (c.loc,(p,None)) in
+      let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
       (match b.v with
       | CProdN (bl,b) -> CProdN (binder::bl,b)
       | _ -> CProdN ([binder],b))
@@ -943,11 +943,11 @@ and factorize_prod scopes vars na bk aty c =
       | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b)
            when binding_kind_eq bk bk' && constr_expr_eq aty ty
                 && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
-         CProdN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+         CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
       | _, CProdN (bl,b) ->
-         CProdN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+         CProdN (CLocalAssum([make na],Default bk,aty)::bl,b)
       | _, _ ->
-         CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
+         CProdN ([CLocalAssum([make na],Default bk,aty)],c)
 
 and factorize_lambda inctx scopes vars na bk aty c =
   let store, get = set_temporary_memory () in
@@ -960,7 +960,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = sub_extern inctx scopes vars b in
       let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
-      let binder = CLocalPattern (c.loc,(p,None)) in
+      let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
       (match b.v with
       | CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
       | _ -> CLambdaN ([binder],b))
@@ -971,11 +971,11 @@ and factorize_lambda inctx scopes vars na bk aty c =
       | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b)
            when binding_kind_eq bk bk' && constr_expr_eq aty ty
                 && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
-         CLambdaN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b)
+         CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b)
       | CLambdaN (bl,b) ->
-         CLambdaN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b)
+         CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b)
       | _ ->
-         CLambdaN ([CLocalAssum([Loc.tag na],Default bk,aty)],c)
+         CLambdaN ([CLocalAssum([make na],Default bk,aty)],c)
 
 and extern_local_binder scopes vars = function
     [] -> ([],[],[])
@@ -985,7 +985,7 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) =
         extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
       (assums,na::ids,
-       CLocalDef((Loc.tag na), extern false scopes vars bd,
+       CLocalDef(CAst.make na, extern false scopes vars bd,
                    Option.map (extern false scopes vars) ty) :: l)
 
     | GLocalAssum (na,bk,ty) ->
@@ -996,21 +996,21 @@ and extern_local_binder scopes vars = function
               match na with Name id -> not (occur_var_constr_expr id ty')
                 | _ -> true ->
               (na::assums,na::ids,
-               CLocalAssum((Loc.tag na)::nal,k,ty')::l)
+               CLocalAssum(CAst.make na::nal,k,ty')::l)
         | (assums,ids,l) ->
             (na::assums,na::ids,
-             CLocalAssum([(Loc.tag na)],Default bk,ty) :: l))
+             CLocalAssum([CAst.make na],Default bk,ty) :: l))
 
     | GLocalPattern ((p,_),_,bk,ty) ->
       let ty =
         if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
       let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in
       let (assums,ids,l) = extern_local_binder scopes vars l in
-      (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
+      (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l)
 
 and extern_eqn inctx scopes vars (loc,(ids,pll,c)) =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
-  Loc.tag ?loc (pll,extern inctx scopes vars c)
+  make ?loc (pll,extern inctx scopes vars c)
 
 and extern_notation (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 694bec897..d03aa3552 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -9,6 +9,7 @@
 open Pp
 open CErrors
 open Util
+open CAst
 open Names
 open Nameops
 open Namegen
@@ -328,8 +329,8 @@ let impls_term_list ?(args = []) =
   in aux []
 
 (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *)
-let rec check_capture ty = function
-  | (loc,Name id)::(_,Name id')::_ when occur_glob_constr id ty ->
+let rec check_capture ty = let open CAst in function
+  | { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty ->
       raise (InternalizationError (loc,VariableCapture (id,id')))
   | _::nal ->
       check_capture ty nal
@@ -360,22 +361,23 @@ let check_hidden_implicit_parameters ?loc id impls =
       strbrk "the type of a constructor shall use a different name.")
 
 let push_name_env ?(global_level=false) ntnvars implargs env =
+  let open CAst in
   function
-  | loc,Anonymous ->
+  | { loc; v = Anonymous } ->
       if global_level then
 	user_err ?loc (str "Anonymous variables not allowed");
       env
-  | loc,Name id ->
+  | { loc; v = Name id } ->
       check_hidden_implicit_parameters ?loc id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
       set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
-      if global_level then Dumpglob.dump_definition (loc,id) true "var"
+      if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var"
       else Dumpglob.dump_binding ?loc id;
       {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
 let intern_generalized_binder ?(global_level=false) intern_type ntnvars
-    env (loc, na) b b' t ty =
+    env {loc;v=na} b b' t ty =
   let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
     if t then ty, ids else
@@ -385,11 +387,11 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
   let ty' = intern_type {env with ids = ids; unb = true} ty in
   let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
   let env' = List.fold_left
-    (fun env (l, x) -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (l, Name x))
+    (fun env {loc;v=x} -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x))
     env fvs in
   let bl = List.map
-    (fun (loc, id) ->
-      (loc, (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+    CAst.(map (fun id ->
+      (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -404,7 +406,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
-  in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl
+  in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl
 
 let intern_assumption intern ntnvars env nal bk ty =
   let intern_type env = intern (set_type_scope env) in
@@ -414,9 +416,9 @@ let intern_assumption intern ntnvars env nal bk ty =
       check_capture ty nal;
       let impls = impls_type_list ty in
       List.fold_left
-	(fun (env, bl) (loc, na as locna) ->
+        (fun (env, bl) ({loc;v=na} as locna) ->
           (push_name_env ntnvars impls env locna,
-           (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl))
+           (make ?loc (na,k,locate_if_hole ?loc na ty))::bl))
 	(env, []) nal
   | Generalized (b,b',t) ->
      let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in
@@ -434,7 +436,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
 
 let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
 
-let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) =
+let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) =
   let term = intern env def in
   let ty = Option.map (intern env) ty in
   (push_name_env ntnvars (impls_term_list term) env locna,
@@ -448,22 +450,22 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p =
       user_err ?loc (str "Unsupported nested \"as\" clause.");
     il,disjpat
   in
-  let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in
+  let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in
   let na = alias_of_pat (List.hd disjpat) in
   let ienv = Name.fold_right Id.Set.remove na env.ids in
   let id = Namegen.next_name_away_with_default "pat" na ienv in
-  let na = (loc, Name id) in
+  let na = make ?loc @@ Name id in
   env,((disjpat,il),id),na
 
 let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function
   | CLocalAssum(nal,bk,ty) ->
       let env, bl' = intern_assumption intern ntnvars env nal bk ty in
-      let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
+      let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in
       env, bl' @ bl
-  | CLocalDef((loc,na as locna),def,ty) ->
+  | CLocalDef( {loc; v=na} as locna,def,ty) ->
      let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in
      env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl
-  | CLocalPattern (loc,(p,ty)) ->
+  | CLocalPattern {loc;v=(p,ty)} ->
       let tyc =
         match ty with
         | Some ty -> ty
@@ -472,8 +474,8 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func
       let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
       let bk = Default Explicit in
       let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
-      let _,(_,bk,t) = List.hd bl' in
-      (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map snd il),id,bk,t)) :: bl)
+      let {v=(_,bk,t)} = List.hd bl' in
+      (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
 
 let intern_generalization intern env ntnvars loc bk ak c =
   let c = intern {env with unb = true} c in
@@ -495,16 +497,16 @@ let intern_generalization intern env ntnvars loc bk ak c =
           | None -> false
       in
 	if pi then
-	  (fun (loc', id) acc ->
+          (fun {loc=loc';v=id} acc ->
             DAst.make ?loc:(Loc.merge_opt loc' loc) @@
 	    GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
 	else
-	  (fun (loc', id) acc ->
+          (fun {loc=loc';v=id} acc ->
             DAst.make ?loc:(Loc.merge_opt loc' loc) @@
 	    GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
     in
-      List.fold_right (fun (loc, id as lid) (env, acc) ->
-        let env' = push_name_env ntnvars (Variable,[],[],[]) env (loc, Name id) in
+      List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
+        let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
 	  (env', abs lid acc)) fvs (env,c)
   in c'
 
@@ -571,7 +573,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
     let pat, na = match disjpat with
     | [pat] when is_var store pat -> let na = get () in None, na
-    | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+    | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
     (renaming,env), pat, na
   with Not_found ->
   try
@@ -581,7 +583,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     if onlyident then
       (* Do not try to interpret a variable as a constructor *)
       let na = out_var pat in
-      let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in
+      let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in
       (renaming,env), None, na
     else
       (* Interpret as a pattern *)
@@ -589,7 +591,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
       let pat, na =
         match disjpat with
         | [pat] when is_var store pat -> let na = get () in None, na
-        | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+        | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in
       (renaming,env), pat, na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
@@ -601,7 +603,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     (renaming',env), None, Name id'
 
 type binder_action =
-| AddLetIn of Name.t Loc.located * constr_expr * constr_expr option
+| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
 | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
 | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
 | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -692,7 +694,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       let knd = match knd with
       | Evar_kinds.BinderType (Name id as na) ->
         let na =
-          try snd (coerce_to_name (fst (Id.Map.find id terms)))
+          try (coerce_to_name (fst (Id.Map.find id terms))).v
           with Not_found ->
           try Name (Id.Map.find id renaming)
           with Not_found -> na
@@ -800,7 +802,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
    into a substitution for interpretation and based on binding/constr
    distinction *)
 
-let cases_pattern_of_name (loc,na) =
+let cases_pattern_of_name {loc;v=na} =
   let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in
   CAst.make ?loc (CPatAtom atom)
 
@@ -898,7 +900,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in
     let expl_impls = List.map
-      (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+      (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (make ?loc @@ ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
     Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
     gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
@@ -958,7 +960,7 @@ let check_no_explicitation l =
   match l with
   | [] -> ()
   | (_, None) :: _ -> assert false
-  | (_, Some (loc, _)) :: _ ->
+  | (_, Some {loc}) :: _ ->
     user_err ?loc  (str"Unexpected explicitation of the argument of an abbreviation.")
 
 let dump_extended_global loc = function
@@ -1034,7 +1036,8 @@ let intern_non_secvar_qualid loc qid intern env ntnvars us args =
     | GRef (VarRef _, _) -> raise Not_found
     | _ -> r
 
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
+let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
+function
   | Qualid (loc, qid) ->
       let r,projapp,args2 =
 	try intern_qualid loc qid intern env ntnvars us args
@@ -1069,11 +1072,11 @@ let interp_reference vars r =
 
 (** Private internalization patterns *)
 type 'a raw_cases_pattern_expr_r =
-  | RCPatAlias of 'a raw_cases_pattern_expr * Name.t Loc.located
+  | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
   | RCPatCstr  of Globnames.global_reference
     * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
   (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
-  | RCPatAtom  of (Id.t Loc.located * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+  | RCPatAtom  of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
   | RCPatOr    of 'a raw_cases_pattern_expr list
 and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
 
@@ -1133,7 +1136,7 @@ let check_number_of_pattern loc n l =
   if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p)))
 
 let check_or_pat_variables loc ids idsl =
-  if List.exists (fun ids' -> not (List.eq_set (fun (loc,id) (_,id') -> Id.equal id id') ids ids')) idsl then
+  if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then
     user_err ?loc  (str
     "The components of this disjunctive pattern must bind the same variables.")
 
@@ -1372,7 +1375,7 @@ let sort_fields ~complete loc fields completer =
 (** {6 Manage multiple aliases} *)
 
 type alias = {
-  alias_ids : Id.t Loc.located list;
+  alias_ids : Misctypes.lident list;
   alias_map : Id.t Id.Map.t;
 }
 
@@ -1383,20 +1386,20 @@ let empty_alias = {
 
   (* [merge_aliases] returns the sets of all aliases encountered at this
      point and a substitution mapping extra aliases to the first one *)
-let merge_aliases aliases (loc,na) =
+let merge_aliases aliases {loc;v=na} =
   match na with
   | Anonymous -> aliases
   | Name id ->
-  let alias_ids = aliases.alias_ids @ [loc,id] in
+  let alias_ids = aliases.alias_ids @ [make ?loc id] in
   let alias_map = match aliases.alias_ids with
   | [] -> aliases.alias_map
-  | (_,id') :: _ -> Id.Map.add id id' aliases.alias_map
+  | {v=id'} :: _ -> Id.Map.add id id' aliases.alias_map
   in
   { alias_ids; alias_map; }
 
 let alias_of als = match als.alias_ids with
 | [] -> Anonymous
-| (_,id) :: _ -> Name id
+| {v=id} :: _ -> Name id
 
 (** {6 Expanding notations }
 
@@ -1426,7 +1429,7 @@ let product_of_cases_patterns aliases idspl =
 
 let rec subst_pat_iterator y t = DAst.(map (function
   | RCPatAtom id as p ->
-    begin match id with Some ((_,x),_) when Id.equal x y -> DAst.get t | _ -> p end
+    begin match id with Some ({v=x},_) when Id.equal x y -> DAst.get t | _ -> p end
   | RCPatCstr (id,l1,l2) ->
     RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
  	       List.map (subst_pat_iterator y t) l2)
@@ -1456,7 +1459,7 @@ let drop_notations_pattern looked_for genv =
   in
   (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
   let rec rcp_of_glob scopes x = DAst.(map (function
-    | GVar id -> RCPatAtom (Some ((x.CAst.loc,id),scopes))
+    | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
     | GHole (_,_,_) -> RCPatAtom (None)
     | GRef (g,_) -> RCPatCstr (g,[],[])
     | GApp (r, l) ->
@@ -1562,7 +1565,7 @@ let drop_notations_pattern looked_for genv =
       begin
 	match drop_syndef top scopes id [] with
 	  | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
-          | None         -> DAst.make ?loc @@ RCPatAtom (Some ((loc,find_pattern_variable id),scopes))
+          | None         -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
       end
     | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
     | CPatOr pl     -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
@@ -1592,7 +1595,7 @@ let drop_notations_pattern looked_for genv =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-          if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((loc,id),scopes)) else
+          if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".")
       end
     | NRef g ->
@@ -1632,7 +1635,7 @@ let rec intern_pat genv ntnvars aliases pat =
     let pl' = List.map (fun (asubst,pl) ->
       (asubst, DAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
-  let loc = CAst.(pat.loc) in
+  let loc = pat.loc in
   match DAst.get pat with
     | RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
@@ -1649,8 +1652,8 @@ let rec intern_pat genv ntnvars aliases pat =
 	let with_letin, pl2 =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
-    | RCPatAtom (Some ((loc,id),scopes)) ->
-      let aliases = merge_aliases aliases (loc,Name id) in
+    | RCPatAtom (Some ({loc;v=id},scopes)) ->
+      let aliases = merge_aliases aliases (make ?loc @@ Name id) in
       set_var_scope ?loc id false scopes ntnvars;
       (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *)
     | RCPatAtom (None) ->
@@ -1696,12 +1699,12 @@ let intern_ind_pattern genv ntnvars scopes pat =
 
 let merge_impargs l args =
   let test x = function
-  | (_, Some (_, y)) -> explicitation_eq x y
+  | (_, Some {v=y}) -> explicitation_eq x y
   | _ -> false
   in
   List.fold_right (fun a l ->
     match a with
-      | (_,Some (_,(ExplByName id as x))) when
+      | (_, Some {v=ExplByName id as x}) when
 	  List.exists (test x) args -> l
       | _ -> a::l)
     l args
@@ -1733,7 +1736,7 @@ let extract_explicit_arg imps args =
       let (eargs,rargs) = aux l in
       match e with
       | None -> (eargs,a::rargs)
-      | Some (loc,pos) ->
+      | Some {loc;v=pos} ->
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
@@ -1772,8 +1775,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	in
 	  apply_impargs c env imp subscopes l loc
 
-    | CFix ((locid,iddef), dl) ->
-        let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
+    | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+        let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
 	  try List.index0 Id.equal iddef lf
@@ -1808,7 +1811,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 					     let (_,bli,tyi,_) = idl_temp.(i) in
 					     let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
 					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
-					    en (Loc.tag @@ Name name)) 0 env' lf in
+                                            en (CAst.make @@ Name name)) 0 env' lf in
              (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
 	DAst.make ?loc @@
           GRec (GFix
@@ -1817,8 +1820,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
               Array.map (fun (_,bl,_,_) -> bl) idl,
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
-    | CCoFix ((locid,iddef), dl) ->
-        let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
+    | CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
+        let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
         let dl = Array.of_list dl in
 	let n =
           try List.index0 Id.equal iddef lf
@@ -1826,7 +1829,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	    raise (InternalizationError (locid,UnboundFixName (true,iddef)))
 	in
         let idl_tmp = Array.map
-          (fun ((loc,id),bl,ty,_) ->
+          (fun ({ CAst.loc; v = id },bl,ty,_) ->
             let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in
             (List.rev (List.map glob_local_binder_of_extended rbl),
              intern_type env' ty,env')) dl in
@@ -1835,7 +1838,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 					     let (bli,tyi,_) = idl_tmp.(i) in
 					     let cofix_args =  List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
 	       push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
-					    en (Loc.tag @@ Name name)) 0 env' lf in
+                                            en (CAst.make @@ Name name)) 0 env' lf in
              (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
 	DAst.make ?loc @@
 	GRec (GCoFix n,
@@ -1856,7 +1859,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
 	DAst.make ?loc @@
-	GLetIn (snd na, inc1, int,
+        GLetIn (na.CAst.v, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
     | CNotation ("- _", ([a],[],[],[])) when is_non_zero a ->
       let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in
@@ -1919,7 +1922,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
-            (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na)
+            (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)
 	    inb) Id.Set.empty tms in
         (* as, in & return vars *)
         let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
@@ -1929,7 +1932,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	    (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
 	  tms ([],Id.Set.empty,[]) in
         let env' = Id.Set.fold
-	  (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.tag @@ Name var))
+          (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var))
 	  (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
         (* PatVars before a real pattern do not need to be matched *)
         let stripped_match_from_in =
@@ -1969,17 +1972,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
-	    (Loc.tag na') in
+            (CAst.make na') in
 	  intern_type env'' u) po in
 	DAst.make ?loc @@
-        GLetTuple (List.map snd nal, (na', p'), b',
+        GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
                    intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
           let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
-	    (Loc.tag na') in
+            (CAst.make na') in
 	  intern_type env'' p) po in
 	DAst.make ?loc @@
         GIf (c', (na', p'), intern env b1, intern env b2)
@@ -2063,10 +2066,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     (ids,List.flatten mpl')
 
   (* Expands a pattern-matching clause [lhs => rhs] *)
-  and intern_eqn n env (loc,(lhs,rhs)) =
+  and intern_eqn n env {loc;v=(lhs,rhs)} =
     let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
-    let eqn_ids = List.map snd eqn_ids in
+    let eqn_ids = List.map (fun x -> x.v) eqn_ids in
     check_linearity lhs eqn_ids;
     let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
     List.map (fun (asubst,pl) ->
@@ -2081,10 +2084,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     let extra_id,na =
       let loc = tm'.CAst.loc in
       match DAst.get tm', na with
-      | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
-      | GRef (VarRef id, _), None -> Some id,(loc,Name id)
-      | _, None -> None,(Loc.tag Anonymous)
-      | _, Some (loc,na) -> None,(loc,na) in
+      | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id, CAst.make ?loc @@ Name id
+      | GRef (VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id
+      | _, None -> None, CAst.make Anonymous
+      | _, Some ({ CAst.loc; v = na } as lna) -> None, lna in
     (* the "in" part *)
     let match_td,typ = match t with
     | Some t ->
@@ -2100,8 +2103,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	let (match_to_do,nal) =
 	  let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
 	    let add_name l = function
-	      | _,Anonymous -> l
-	      | loc,(Name y as x) -> (y, DAst.make ?loc @@ PatVar x) :: l in
+              | { CAst.v = Anonymous } -> l
+              | { CAst.loc; v = (Name y as x) } -> (y, DAst.make ?loc @@ PatVar x) :: l in
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
@@ -2113,7 +2116,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                 | PatVar x ->
                   let loc = c.CAst.loc in
                   canonize_args t tt forbidden_names
-                    (add_name match_acc (loc,x)) ((loc,x)::var_acc)
+                    (add_name match_acc CAst.(make ?loc x)) ((loc,x)::var_acc)
                 | _ ->
                   let fresh =
                     Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
@@ -2127,7 +2130,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
     | None ->
       [], None in
-    (tm',(snd na,typ)), extra_id, match_td
+    (tm',(na.CAst.v,typ)), extra_id, match_td
 
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
@@ -2169,7 +2172,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     in aux 1 l subscopes eargs rargs
 
   and apply_impargs c env imp subscopes l loc =
-    let l : (Constrexpr.constr_expr * Constrexpr.explicitation Loc.located option) list = l in
     let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
     let l = intern_impargs c env imp subscopes l in
       smart_gapp c loc l
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f09b17a49..7411fb84b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-  Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list
+  lident list * (Id.t Id.Map.t * cases_pattern) list
 
 val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
 
diff --git a/interp/declare.ml b/interp/declare.ml
index 72cdabfd2..dfa84f278 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -561,7 +561,7 @@ let do_universe poly l =
                    (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
-    List.map (fun (l, id) ->
+    List.map (fun {CAst.v=id} ->
       let lev = Universes.new_univ_id () in
       (id, lev)) l
   in
diff --git a/interp/declare.mli b/interp/declare.mli
index f368d164e..9bec32d29 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -85,6 +85,6 @@ val declare_univ_binders : Globnames.global_reference -> Universes.universe_bind
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
-val do_universe : polymorphic -> Id.t Loc.located list -> unit
+val do_universe : polymorphic -> Misctypes.lident list -> unit
 val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
                     unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index d7962e29a..e439db2b2 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -249,12 +249,12 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc ->
     dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id)
   ) loc
 
-let dump_definition (loc, id) sec s =
+let dump_definition {CAst.loc;v=id} sec s =
   dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
 
-let dump_constraint (((loc, n),_), _, _) sec ty =
+let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty =
   match n with
-    | Names.Name id -> dump_definition (loc, id) sec ty
+    | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty
     | Names.Anonymous -> ()
 
 let dump_moddef ?loc mp ty =
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index f3ad50f28..c779e860f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -25,7 +25,7 @@ val continue : unit -> unit
 val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
 val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
 
-val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit
+val dump_definition : Misctypes.lident -> bool -> string -> unit
 val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_modref  : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_reference  : ?loc:Loc.t -> string -> string -> string -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a838d7106..326969b67 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -26,7 +26,7 @@ module RelDecl = Context.Rel.Declaration
 
 let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
 
-let declare_generalizable_ident table (loc,id) =
+let declare_generalizable_ident table {CAst.loc;v=id} =
   if not (Id.equal id (root_of_id id)) then
     user_err ?loc ~hdr:"declare_generalizable_ident"
     ((Id.print id ++ str
@@ -49,7 +49,7 @@ let cache_generalizable_type (_,(local,cmd)) =
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
 
-let in_generalizable : bool * Id.t Loc.located list option -> obj =
+let in_generalizable : bool * Misctypes.lident list option -> obj =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
@@ -99,7 +99,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   in aux bound l c
 
 let ids_of_names l =
-  List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
+  List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l
 
 let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) =
   let rec aux bdvars l c = match c with
@@ -109,7 +109,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
     | ((CLocalDef (n, c, t)) :: tl) ->
-	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
+        let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
 	let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in
 	  aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl
@@ -123,13 +123,13 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
     | GVar id ->
         let loc = c.CAst.loc in
 	if is_freevar bound (Global.env ()) id then
-	  if Id.List.mem_assoc_sym id vs then vs
-	  else (Loc.tag ?loc id) :: vs
+          if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs
+          else CAst.(make ?loc id) :: vs
 	else vs
     | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
   in fun rt -> 
     let vars = List.rev (vars bound [] rt) in
-      List.iter (fun (loc, id) ->
+      List.iter (fun {CAst.loc;v=id} ->
 	if not (Id.Set.mem id allowed || find_generalizable_ident id) then 
 	  ungeneralizable loc id) vars;
       vars
@@ -146,7 +146,7 @@ let combine_params avoid fn applied needed =
   let named, applied =
     List.partition
       (function
-	  (t, Some (loc, ExplByName id)) ->
+          (t, Some {CAst.loc;v=ExplByName id}) ->
             let is_id (_, decl) = match RelDecl.get_name decl with
             | Name id' -> Id.equal id id'
             | Anonymous -> false
@@ -157,7 +157,7 @@ let combine_params avoid fn applied needed =
 	| _ -> false) applied
   in
   let named = List.map
-    (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false)
+    (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false)
     named
   in
   let is_unset (_, decl) = match decl with
@@ -198,23 +198,23 @@ let destClassApp cl =
   let open CAst in
   let loc = cl.loc in
   match cl.v with
-    | CApp ((None, { v = CRef (ref, inst) }), l) -> Loc.tag ?loc (ref, List.map fst l, inst)
-    | CAppExpl ((None, ref, inst), l) -> Loc.tag ?loc (ref, l, inst)
-    | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst)
+    | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst)
+    | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst)
+    | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst)
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
   let open CAst in
   let loc = cl.loc in
   match cl.v with
-    | CApp ((None, { v = CRef (ref, inst) } ), l) -> Loc.tag ?loc (ref, l, inst)
-    | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst)
+    | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst)
+    | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst)
     | _ -> raise Not_found
 
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let (_, (r, _, _) as clapp) = destClassAppExpl ty in
+      let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in
       let (loc, qid) = qualid_of_reference r in
       let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -222,7 +222,7 @@ let implicit_application env ?(allow_partial=true) f ty =
   in
     match is_class with
     | None -> ty, env
-    | Some ((loc, (id, par, inst)), gr) ->
+    | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
 	  let c = class_info gr in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index bfe73160b..625e12003 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -6,18 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Glob_term
 open Constrexpr
 open Libnames
 open Globnames
 
-val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
+val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) located
-val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation located option) list * instance_expr option) located
+val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
+val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
@@ -31,7 +30,7 @@ val free_vars_of_binders :
    order with the location of their first occurrence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
-  glob_constr -> Id.t located list
+  glob_constr -> Misctypes.lident list
 
 val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 04710282f..3e1a7dd9b 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -84,7 +84,7 @@ let in_reserved : Id.t * notation_constr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
-let declare_reserved_type_binding (loc,id) t =
+let declare_reserved_type_binding {CAst.loc;v=id} t =
   if not (Id.equal id (root_of_id id)) then
     user_err ?loc ~hdr:"declare_reserved_type"
       ((Id.print id ++ str
diff --git a/interp/reserve.mli b/interp/reserve.mli
index 4fcef23c5..5899cd628 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -6,9 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Notation_term
 
-val declare_reserved_type : Id.t located list -> notation_constr -> unit
+val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit
 val find_reserved_type : Id.t -> notation_constr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index ed00fe296..ea1c63b89 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -41,7 +41,7 @@ val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and
 
 val wit_ident : Id.t uniform_genarg_type
 
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+val wit_var : (lident, lident, Id.t) genarg_type
 
 val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
 
@@ -76,7 +76,7 @@ val wit_red_expr :
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
-val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_clause_dft_concl :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
 
 (** Aliases for compatibility *)
 
@@ -84,7 +84,7 @@ val wit_integer : int uniform_genarg_type
 val wit_preident : string uniform_genarg_type
 val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type
 val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
-val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
+val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
 val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
 val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 val wit_redexpr :
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 9fc02461e..66d87707c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Constrexpr
 
@@ -15,7 +14,7 @@ val asymmetric_patterns : bool ref
 [@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"]
 
 (** Utilities on constr_expr *)
-val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list
+val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list
 [@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"]
 
 val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list