[location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.

6 files changed, 171 insertions, 156 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index ce349a63f..b11972cd3 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -59,9 +59,9 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
 
 let eq_located f (_, x) (_, y) = f x y
 
-let rec cases_pattern_expr_eq (l1, p1) (l2, p2) =
-  if p1 == p2 then true
-  else match p1, p2 with
+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) ->
       Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
@@ -97,9 +97,9 @@ let eq_universes u1 u2 =
   | Some l, Some l' -> l = l'
   | _, _ -> false
 
-let rec constr_expr_eq (_loc1, e1) (_loc2, e2) =
-  if e1 == e2 then true
-  else match e1, e2 with
+let rec constr_expr_eq e1 e2 =
+  if CAst.(e1.v == e2.v) then true
+  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 &&
@@ -228,11 +228,11 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
 and instance_eq (x1,c1) (x2,c2) =
   Id.equal x1 x2 && constr_expr_eq c1 c2
 
-let constr_loc (l,_) = l
+let constr_loc c = CAst.(c.loc)
 
-let cases_pattern_expr_loc (l,_) = l
+let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
-let raw_cases_pattern_expr_loc (l, _) = l
+let raw_cases_pattern_expr_loc pe = CAst.(pe.loc)
 
 let local_binder_loc = function
   | CLocalAssum ((loc,_)::_,_,t)
@@ -247,18 +247,18 @@ let local_binders_loc bll = match bll with
 
 (** Pseudo-constructors *)
 
-let mkIdentC id   = Loc.tag @@ CRef (Ident (Loc.tag id),None)
-let mkRefC r      = Loc.tag @@ CRef (r,None)
-let mkCastC (a,k) = Loc.tag @@ CCast (a,k)
-let mkLambdaC (idl,bk,a,b) = Loc.tag @@ CLambdaN ([idl,bk,a],b)
-let mkLetInC  (id,a,t,b)   = Loc.tag @@ CLetIn (id,a,t,b)
-let mkProdC   (idl,bk,a,b) = Loc.tag @@ CProdN ([idl,bk,a],b)
+let mkIdentC id   = CAst.make @@ CRef (Ident (Loc.tag id),None)
+let mkRefC r      = CAst.make @@ CRef (r,None)
+let mkCastC (a,k) = CAst.make @@ CCast (a,k)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b)
+let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
+let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
-  match f with
-  | _loc, CApp (g,l') -> Loc.tag @@ CApp (g, l' @ l)
-  | _                 -> Loc.tag @@ CApp ((None, f), l)
+  match CAst.(f.v) with
+  | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
+  | _           -> CAst.make @@ CApp ((None, f), l)
 
 let add_name_in_env env n =
   match snd n with
@@ -276,7 +276,7 @@ let expand_binders ?loc mkC bl c =
         | CLocalDef ((loc1,_) as n, oty, b) ->
             let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
             let env = add_name_in_env env n in
-            (env, Loc.tag ?loc @@ CLetIn (n,oty,b,c))
+            (env, CAst.make ?loc @@ CLetIn (n,oty,b,c))
         | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
             let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
             let env = List.fold_left add_name_in_env env nl in
@@ -288,10 +288,10 @@ let expand_binders ?loc mkC bl c =
             let id = (loc1, Name ni) in
             let ty = match ty with
                  | Some ty -> ty
-                 | None -> Loc.tag ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
+                 | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
             in
-            let e = Loc.tag @@ CRef (Libnames.Ident (loc1, ni), None) in
-            let c = Loc.tag ?loc @@
+            let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in
+            let c = CAst.make ?loc @@
               CCases
                 (LetPatternStyle, None, [(e,None,None)],
                  [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))])
@@ -302,11 +302,11 @@ let expand_binders ?loc mkC bl c =
   c
 
 let mkCProdN ?loc bll c =
-  let mk ?loc b c = Loc.tag ?loc @@ CProdN ([b],c) in
+  let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in
   expand_binders ?loc mk bll c
 
 let mkCLambdaN ?loc bll c =
-  let mk ?loc b c = Loc.tag ?loc @@ CLambdaN ([b],c) in
+  let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in
   expand_binders ?loc mk bll c
 
 (* Deprecated *)
@@ -320,14 +320,13 @@ let coerce_reference_to_id = function
         (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
-  | _loc, CRef (Ident (loc,id),_) -> (loc,id)
-  | a -> CErrors.user_err ?loc:(constr_loc a)
+  | { CAst.v = CRef (Ident (loc,id),_); _ } -> (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
-  | _loc, CRef (Ident (loc,id),_) -> (loc,Name id)
-  | loc, CHole (_,_,_) -> (loc,Anonymous)
-  | a -> CErrors.user_err
-         ?loc:(constr_loc a) ~hdr:"coerce_to_name"
-         (str "This expression should be a name.")
+  | { CAst.v = CRef (Ident (loc,id),_) } -> (loc,Name id)
+  | { CAst.loc; CAst.v = CHole (_,_,_) } -> (loc,Anonymous)
+  | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
+                         (str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 30b81ecc4..e8a5b5265 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -144,15 +144,15 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
 
 let insert_delimiters e = function
   | None -> e
-  | Some sc -> Loc.tag @@ CDelimiters (sc,e)
+  | Some sc -> CAst.make @@ CDelimiters (sc,e)
 
 let insert_pat_delimiters ?loc p = function
   | None -> p
-  | Some sc -> Loc.tag ?loc @@ CPatDelimiters (sc,p)
+  | Some sc -> CAst.make ?loc @@ CPatDelimiters (sc,p)
 
 let insert_pat_alias ?loc p = function
   | Anonymous -> p
-  | Name id -> Loc.tag ?loc @@ CPatAlias (p,id)
+  | Name id -> CAst.make ?loc @@ CPatAlias (p,id)
 
 (**********************************************************************)
 (* conversion of references                                           *)
@@ -178,7 +178,7 @@ let extern_reference ?loc vars l = !my_extern_reference ?loc vars l
 
 let add_patt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (Loc.tag @@ CPatAtom None) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
 
 let add_cpatt_for_params ind l =
   if !Flags.in_debugger then l else
@@ -190,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args =
   let rec impls_fit l = function
     |[],t -> Some (List.rev_append l t)
     |_,[] -> None
-    |h::t,(_loc, CPatAtom None)::tt when is_status_implicit h -> impls_fit l (t,tt)
+    |h::t, { CAst.v = CPatAtom None }::tt when is_status_implicit h -> impls_fit l (t,tt)
     |h::_,_ when is_status_implicit h -> None
     |_::t,hh::tt -> impls_fit (hh::l) (t,tt)
   in let rec aux = function
@@ -236,8 +236,8 @@ let expand_curly_brackets loc mknot ntn l =
   (* side effect *)
   mknot (loc,!ntn',l)
 
-let destPrim = function _loc, CPrim t -> Some t | _ -> None
-let destPatPrim = function _loc, CPatPrim t -> Some t | _ -> None
+let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
+let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 
 let make_notation_gen loc ntn mknot mkprim destprim l =
   if has_curly_brackets ntn
@@ -259,21 +259,21 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
 
 let make_notation loc ntn (terms,termlists,binders as subst) =
   if not (List.is_empty termlists) || not (List.is_empty binders) then
-    Loc.tag ?loc @@ CNotation (ntn,subst)
+    CAst.make ?loc @@ CNotation (ntn,subst)
   else
     make_notation_gen loc ntn
-      (fun (loc,ntn,l) -> Loc.tag ?loc @@ CNotation (ntn,(l,[],[])))
-      (fun (loc,p) -> Loc.tag ?loc @@ CPrim p)
+      (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[])))
+      (fun (loc,p) -> CAst.make ?loc @@ CPrim p)
       destPrim terms
 
 let make_pat_notation ?loc ntn (terms,termlists as subst) args =
-  if not (List.is_empty termlists) then (Loc.tag ?loc @@ CPatNotation (ntn,subst,args)) else
+  if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else
   make_notation_gen loc ntn
-    (fun (loc,ntn,l) -> Loc.tag ?loc @@ CPatNotation (ntn,(l,[]),args))
-    (fun (loc,p)     -> Loc.tag ?loc @@ CPatPrim p)
+    (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
+    (fun (loc,p)     -> CAst.make ?loc @@ CPatPrim p)
     destPatPrim terms
 
-let mkPat ?loc qid l = Loc.tag ?loc @@
+let mkPat ?loc qid l = CAst.make ?loc @@
   (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
   if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l)
 
@@ -295,7 +295,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
       let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
+      CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
     | _ ->
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       | None -> raise No_match
       | Some key ->
 	let loc = cases_pattern_loc pat in
-	insert_pat_alias ?loc (insert_pat_delimiters ?loc (Loc.tag ?loc @@ CPatPrim p) key) na
+	insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na
   with No_match ->
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -312,8 +312,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 	(uninterp_cases_pattern_notations pat)
     with No_match ->
       match pat with
-	| loc, PatVar (Name id)   -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id)))
-	| loc, PatVar (Anonymous) -> Loc.tag ?loc @@ CPatAtom None
+	| loc, PatVar (Name id)   -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id)))
+	| loc, PatVar (Anonymous) -> CAst.make ?loc @@ CPatAtom None
 	| loc, PatCstr(cstrsp,args,na) ->
 	  let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
 	  let p =
@@ -327,24 +327,29 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		  | Some c :: q ->
 		    match args with
 		      | [] -> raise No_match
-		      | (_loc, CPatAtom(None)) :: tail -> ip q tail acc
+
+
+
+
+
+	| { CAst.v = CPatAtom None } :: tail -> ip q tail acc
 		    (* we don't want to have 'x = _' in our patterns *)
 		      | head :: tail -> ip q tail
 		        ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
 	      in
-	      Loc.tag ?loc @@ CPatRecord(List.rev (ip projs args []))
+	      CAst.make ?loc @@ CPatRecord(List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
                   let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in
 		  if !Topconstr.asymmetric_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
-		    then Loc.tag ?loc @@ CPatCstr (c, None, args)
-		    else Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
+		    then CAst.make ?loc @@ CPatCstr (c, None, args)
+		    else CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
 		  else
 		    let full_args = add_patt_for_params (fst cstrsp) args in
 		    match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
-		      | Some true_args -> Loc.tag ?loc @@ CPatCstr (c, None, true_args)
-		      | None           -> Loc.tag ?loc @@ CPatCstr (c, Some full_args, [])
+		      | Some true_args -> CAst.make ?loc @@ CPatCstr (c, None, true_args)
+		      | None           -> CAst.make ?loc @@ CPatCstr (c, Some full_args, [])
 	  in insert_pat_alias ?loc p na
 and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
     (tmp_scope, scopes as allscopes) vars =
@@ -401,8 +406,8 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = func
 	  let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
 	    (match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in
 	  insert_pat_alias ?loc p na
-	| PatVar Anonymous -> Loc.tag ?loc @@ CPatAtom None
-	| PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id)))
+	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
+	| PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id)))
     with
 	No_match -> extern_notation_pattern allscopes vars (loc, t) rules
 
@@ -422,7 +427,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
   if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
     let c = extern_reference vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-    Loc.tag @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
+    CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -430,7 +435,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       match availability_of_prim_token p sc scopes with
 	| None -> raise No_match
 	| Some key ->
-	  insert_pat_delimiters (Loc.tag @@ CPatPrim p) key
+	  insert_pat_delimiters (CAst.make @@ CPatPrim p) key
     with No_match ->
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -440,8 +445,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       let c = extern_reference vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       match drop_implicits_in_patt (IndRef ind) 0 args with
-	   |Some true_args -> Loc.tag @@ CPatCstr (c, None, true_args)
-	   |None           -> Loc.tag @@ CPatCstr (c, Some args, [])
+	   |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
+	   |None           -> CAst.make @@ CPatCstr (c, Some args, [])
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
@@ -466,7 +471,7 @@ let is_projection nargs = function
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
 let is_significant_implicit a =
-  not (is_hole (snd a))
+  not (is_hole (a.CAst.v))
 
 let is_needed_for_correct_partial_application tail imp =
   List.is_empty tail && not (maximal_insertion_of imp)
@@ -515,11 +520,11 @@ let explicitize inctx impl (cf,f) args =
 	  CApp ((ip,f),args1@args2)
     | None ->
       let args = exprec 1 (args,impl) in
-	if List.is_empty args then snd f else CApp ((None, f), args)
+	if List.is_empty args then f.CAst.v else CApp ((None, f), args)
   in
     try expl ()
     with Expl -> 
-      let f',us = match f with (_loc, CRef (f,us)) -> f,us | _ -> assert false in
+      let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
       let ip = if !print_projections then ip else None in
 	CAppExpl ((ip, f', us), List.map Lazy.force args)
 
@@ -546,7 +551,7 @@ let extern_app inctx impl (cf,f) us args =
     let args = List.map Lazy.force args in
     CAppExpl ((is_projection (List.length args) cf,f,us), args)
   else
-    explicitize inctx impl (cf, Loc.tag @@ CRef (f,us)) args
+    explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
 
 let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
 | [], _ -> []
@@ -600,7 +605,7 @@ let extern_possible_prim_token scopes r =
     let (sc,n) = uninterp_prim_token r in
     match availability_of_prim_token n sc scopes with
     | None -> None
-    | Some key -> Some (insert_delimiters (Loc.tag ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
+    | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
   with No_match ->
     None
 
@@ -608,7 +613,7 @@ let extern_optimal_prim_token scopes r r' =
   let c = extern_possible_prim_token scopes r in
   let c' = if r==r' then None else extern_possible_prim_token scopes r' in
   match c,c' with
-  | Some n, (Some ((_, CDelimiters _)) | None) | _, Some n -> n
+  | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
   | _ -> raise No_match
 
 (**********************************************************************)
@@ -644,7 +649,7 @@ let rec extern inctx scopes vars r =
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_notation scopes vars r'' (uninterp_notations r'')
-  with No_match -> Loc.map_with_loc (fun ?loc -> function
+  with No_match -> CAst.map_from_loc (fun ?loc -> function
   | GRef (ref,us) ->
       extern_global (select_stronger_impargs (implicits_of_global ref))
         (extern_reference ?loc vars ref) (extern_universes us)
@@ -824,7 +829,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 and factorize_prod scopes vars na bk aty c =
   let c = extern_typ scopes vars c in
   match na, c with
-  | Name id, (loc, CProdN ([nal,Default bk',ty],c))
+  | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) }
       when binding_kind_eq bk bk' && constr_expr_eq aty ty
       && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
       nal,c
@@ -834,7 +839,7 @@ and factorize_prod scopes vars na bk aty c =
 and factorize_lambda inctx scopes vars na bk aty c =
   let c = sub_extern inctx scopes vars c in
   match c with
-  | loc, CLambdaN ([nal,Default bk',ty],c)
+  | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) }
       when binding_kind_eq bk bk' && constr_expr_eq aty ty
       && not (occur_name na ty) (* avoid na in ty escapes scope *) ->
       nal,c
@@ -943,12 +948,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
 		  extern true (scopt,scl@scopes) vars c, None)
 		  terms in
               let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in
-	      Loc.tag ?loc @@ if List.is_empty l then a else CApp ((None, Loc.tag a),l) in
+	      CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in
  	if List.is_empty args then e
 	else
 	  let args = fill_arg_scopes args argsscopes scopes in
 	  let args = extern_args (extern true) vars args in
-	  Loc.tag ?loc @@ explicitize false argsimpls (None,e) args
+	  CAst.make ?loc @@ explicitize false argsimpls (None,e) args
       with
 	  No_match -> extern_notation allscopes vars t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a672771b1..541b52972 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -217,7 +217,7 @@ let contract_notation ntn (l,ll,bll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | (_loc, CNotation ("{ _ }",([a],[],[]))) :: l ->
+    | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -230,7 +230,7 @@ let contract_pat_notation ntn (l,ll) =
   let ntn' = ref ntn in
   let rec contract_squash n = function
     | [] -> []
-    | (_, CPatNotation ("{ _ }",([a],[]),[])) :: l ->
+    | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l ->
         ntn' := expand_notation_string !ntn' n;
         contract_squash n (a::l)
     | a :: l ->
@@ -407,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	  let name =
 	    let id =
 	      match ty with
-	      | _, CApp ((_, (_, CRef (Ident (loc,id),_))), _) -> id
+	      | { CAst.v = CApp ((_, { CAst.v = CRef (Ident (loc,id),_) } ), _) } -> id
 	      | _ -> default_non_dependent_ident
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
@@ -430,7 +430,7 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
-let rec free_vars_of_pat il (loc, pt) = match pt with
+let rec free_vars_of_pat il pt = match CAst.(pt.v) with
   | CPatCstr (c, l1, l2) ->
       let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
       List.fold_left free_vars_of_pat il l2
@@ -448,7 +448,7 @@ let intern_local_pattern intern lvar env p =
   List.fold_left
     (fun env (loc, i) ->
        let bk = Default Implicit in
-       let ty = Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
+       let ty = CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
        let n = Name i in
        let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
        env)
@@ -480,7 +480,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
       let tyc =
         match ty with
         | Some ty -> ty
-        | None -> Loc.tag ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+        | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
       let env = intern_local_pattern intern lvar env p in
       let il = List.map snd (free_vars_of_pat [] p) in
@@ -596,16 +596,16 @@ let rec subordinate_letins letins = function
       letins,[]
 
 let terms_of_binders bl =
-  let rec term_of_pat pt = Loc.map_with_loc (fun ?loc -> function
+  let rec term_of_pat pt = CAst.map_from_loc (fun ?loc -> function
     | PatVar (Name id)   -> CRef (Ident (loc,id), None)
     | PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
     | PatCstr (c,l,_) ->
        let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
-       let hole = Loc.tag ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+       let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables = function
-    | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+    | (loc, GLocalAssum (Name id,_,_))::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
     | (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
     | (loc, GLocalDef (Anonymous,_,_,_))::l
     | (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
@@ -760,7 +760,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
   try
     let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
     let expl_impls = List.map
-      (fun id -> Loc.tag ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+      (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (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
@@ -993,10 +993,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,(Loc.tag @@ RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom(None))::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
-      then let (b,out) = aux i (q,l) in (b,(Loc.tag @@ RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out)
       else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
   in aux 0 (impl_list,pl2)
 
@@ -1199,14 +1199,15 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let rec subst_pat_iterator y t (loc, p) = match p with
-  | RCPatAtom id ->
-    begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ?loc p end
+let rec subst_pat_iterator y t = CAst.map (function
+  | RCPatAtom id as p ->
+    begin match id with Some x when Id.equal x y -> t.CAst.v | _ -> p end
   | RCPatCstr (id,l1,l2) ->
-     Loc.tag ?loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
-                                    List.map (subst_pat_iterator y t) l2)
-  | RCPatAlias (p,a) -> Loc.tag ?loc @@ RCPatAlias (subst_pat_iterator y t p,a)
-  | RCPatOr pl       -> Loc.tag ?loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
+    RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
+                   List.map (subst_pat_iterator y t) l2)
+  | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
+  | RCPatOr pl       -> RCPatOr (List.map (subst_pat_iterator y t) pl)
+  )
 
 let drop_notations_pattern looked_for =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1255,26 +1256,29 @@ let drop_notations_pattern looked_for =
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
     with Not_found -> None
-  and in_pat top scopes (loc, pt) = match pt with
-    | CPatAlias (p, id) -> Loc.tag ?loc @@ RCPatAlias (in_pat top scopes p, id)
+  and in_pat top scopes pt =
+    let open CAst in
+    let loc = pt.loc in
+    match pt.v with
+    | CPatAlias (p, id) -> CAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
     | CPatRecord l ->
       let sorted_fields =
-	sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in
+	sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
       begin match sorted_fields with
-	| None -> Loc.tag ?loc @@ RCPatAtom None
+	| None -> CAst.make ?loc @@ RCPatAtom None
 	| Some (n, head, pl) ->
           let pl =
             if !asymmetric_patterns then pl else
-            let pars = List.make n (loc, CPatAtom None) in
+            let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
             List.rev_append pars pl in
 	  match drop_syndef top scopes head pl with
-	    |Some (a,b,c) -> (loc, RCPatCstr(a, b, c))
-	    |None -> raise (InternalizationError (loc,NotAConstructor head))
+	    | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
+	    | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
     | CPatCstr (head, None, pl) ->
       begin
 	match drop_syndef top scopes head pl with
-	  | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr(a, b, c)
+	  | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
      | CPatCstr (r, Some expl_pl, pl) ->
@@ -1283,13 +1287,13 @@ let drop_notations_pattern looked_for =
  	      raise (InternalizationError (loc,NotAConstructor r)) in
       if expl_pl == [] then
         (* Convention: (@r) deactivates all further implicit arguments and scopes *)
-        Loc.tag ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+        CAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
       else
         (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
-        Loc.tag ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
+        CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
 	when Bigint.is_strictly_pos p ->
       fst (Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
     | CPatNotation ("( _ )",([a],[]),[]) ->
@@ -1308,11 +1312,11 @@ let drop_notations_pattern looked_for =
     | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
-	  | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr (a, b, c)
-	  | None         -> Loc.tag ?loc @@ RCPatAtom (Some (find_pattern_variable id))
+	  | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr (a, b, c)
+	  | None         -> CAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id))
       end
-    | CPatAtom None -> Loc.tag ?loc @@ RCPatAtom None
-    | CPatOr pl     -> Loc.tag ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+    | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None
+    | CPatOr pl     -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
     | CPatCast _ ->
       assert false
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
@@ -1326,17 +1330,17 @@ let drop_notations_pattern looked_for =
 	  let (a,(scopt,subscopes)) = Id.Map.find id subst in
 	  in_pat top (scopt,subscopes@snd scopes) a
 	with Not_found ->
-	  if Id.equal id ldots_var then Loc.tag ?loc @@ RCPatAtom (Some id) else
+	  if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else
 	    anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
       end
     | NRef g ->
       ensure_kind top loc g;
       let (_,argscs) = find_remaining_scopes [] args g in
-      Loc.tag ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
+      CAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
     | NApp (NRef g,pl) ->
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
-      Loc.tag ?loc @@ RCPatCstr (g,
+      CAst.make ?loc @@ RCPatCstr (g,
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
@@ -1355,7 +1359,7 @@ let drop_notations_pattern looked_for =
          anomaly (Pp.str "Inconsistent substitution of recursive notation"))
     | NHole _ ->
       let () = assert (List.is_empty args) in
-      Loc.tag ?loc @@ RCPatAtom None
+      CAst.make ?loc @@ RCPatAtom None
     | t -> error_invalid_pattern_notation ?loc ()
   in in_pat true
 
@@ -1366,11 +1370,12 @@ let rec intern_pat genv aliases pat =
     let pl' = List.map (fun (asubst,pl) ->
       (asubst, Loc.tag ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
-  match pat with
-    | loc, RCPatAlias (p, id) ->
+  let loc = CAst.(pat.loc) in
+  match CAst.(pat.v) with
+    | RCPatAlias (p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_pat genv aliases' p
-    | loc, RCPatCstr (head, expl_pl, pl) ->
+    | RCPatCstr (head, expl_pl, pl) ->
       if !asymmetric_patterns then
         let len = if List.is_empty expl_pl then Some (List.length pl) else None in
 	let c,idslpl1 = find_constructor loc len head in
@@ -1382,13 +1387,13 @@ let rec intern_pat genv aliases pat =
 	let with_letin, pl2 =
 	  add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
 	intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
-    | loc, RCPatAtom (Some id) ->
+    | RCPatAtom (Some id) ->
       let aliases = merge_aliases aliases id in
       (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)])
-    | loc, RCPatAtom (None) ->
+    | RCPatAtom (None) ->
       let { alias_ids = ids; alias_map = asubst; } = aliases in
       (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)])
-    | loc, RCPatOr pl ->
+    | RCPatOr pl ->
       assert (not (List.is_empty pl));
       let pl' = List.map (intern_pat genv aliases) pl in
       let (idsl,pl') = List.split pl' in
@@ -1406,9 +1411,9 @@ let rec intern_pat genv aliases pat =
    of lambdas in the encoding of match in constr. We put this check here and not
    in the parser because it would require to duplicate the levels of the
    [pattern] rule. *)
-let rec check_no_patcast (loc, pt) = match pt with
+let rec check_no_patcast pt = match CAst.(pt.v) with
   | CPatCast (_,_) ->
-     CErrors.user_err ?loc ~hdr:"check_no_patcast"
+     CErrors.user_err ?loc:pt.CAst.loc ~hdr:"check_no_patcast"
                            (Pp.strbrk "Casts are not supported here.")
   | CPatDelimiters(_,p)
   | CPatAlias(p,_) -> check_no_patcast p
@@ -1444,8 +1449,9 @@ let intern_ind_pattern genv scopes pat =
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
     with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
   in
-  match no_not with
-    | loc, RCPatCstr (head, expl_pl, pl) ->
+  let loc = no_not.CAst.loc in
+  match no_not.CAst.v with
+    | RCPatCstr (head, expl_pl, pl) ->
       let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
       let with_letin, pl2 = add_implicits_check_ind_length genv loc c
 	(List.length expl_pl) pl in
@@ -1455,7 +1461,7 @@ let intern_ind_pattern genv scopes pat =
        match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
        | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
        | _ -> error_bad_inductive_type ?loc)
-    | x -> error_bad_inductive_type ?loc:(raw_cases_pattern_expr_loc x)
+    | x -> error_bad_inductive_type ?loc
 
 (**********************************************************************)
 (* Utilities for application                                          *)
@@ -1521,7 +1527,7 @@ let extract_explicit_arg imps args =
 (* Main loop                                                          *)
 
 let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
-  let rec intern env = Loc.with_loc (fun ?loc -> function
+  let rec intern env = CAst.with_loc_val (fun ?loc -> function
     | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env (Environ.named_context globalenv)
@@ -1602,20 +1608,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CProdN ([],c2) ->
         intern_type env c2
     | CProdN ((nal,bk,ty)::bll,c2) ->
-        iterate_prod ?loc env bk ty (Loc.tag ?loc @@ CProdN (bll, c2)) nal
+        iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal
     | CLambdaN ([],c2) ->
         intern env c2
     | CLambdaN ((nal,bk,ty)::bll,c2) ->
-	iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ?loc @@ CLambdaN (bll, c2)) nal
+	iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?loc @@ CLambdaN (bll, c2)) nal
     | CLetIn (na,c1,t,c2) ->
 	let inc1 = intern (reset_tmp_scope env) c1 in
 	let int = Option.map (intern_type env) t in
 	Loc.tag ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
+    | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
 	when Bigint.is_strictly_pos p ->
-	intern env (Loc.tag ?loc @@ CPrim (Numeral (Bigint.neg p)))
+	intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p)))
     | CNotation ("( _ )",([a],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
@@ -1639,20 +1645,20 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CApp ((isproj,f), args) ->
         let f,args = match f with
           (* Compact notations like "t.(f args') args" *)
-          | _loc, CApp ((Some _,f), args') when not (Option.has_some isproj) ->
+          | { CAst.v = CApp ((Some _,f), args') } when not (Option.has_some isproj) ->
 	    f,args'@args
           (* Don't compact "(f args') args" to resolve implicits separately *)
           | _ -> f,args in
 	let (c,impargs,args_scopes,l),args =
-          match f with
-            | _loc, CRef (ref,us) -> 
+          match f.CAst.v with
+            | CRef (ref,us) -> 
 	       intern_applied_reference intern env
 		 (Environ.named_context globalenv) lvar us args ref
-            | _loc, CNotation (ntn,([],[],[])) ->
+            | CNotation (ntn,([],[],[])) ->
                 let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
                 let x, impl, scopes, l = find_appl_head_data c in
 		  (x,impl,scopes,l), args
-            | x -> (intern env f,[],[],[]), args in
+            | _ -> (intern env f,[],[],[]), args in
           apply_impargs c env impargs args_scopes
 	    (merge_impargs l args) loc
 
@@ -1660,15 +1666,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> Loc.tag ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
-                                                         Misctypes.IntroAnonymous, None))
+	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+                                                           Misctypes.IntroAnonymous, None))
        in
        begin
 	  match fields with
 	    | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
-                let app = Loc.tag ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
+		let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+                let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
 	  intern env app
 	end
     | CCases (sty, rtnpo, tms, eqns) ->
@@ -1910,6 +1916,7 @@ let internalize globalenv env allow_patvar (_, 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/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index dd04e2030..52a6c450b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,11 +92,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
       else ungeneralizable loc id
     else l
   in
-  let rec aux bdvars l (loc, c) = match c with
+  let rec aux bdvars l c = match CAst.(c.v) with
     | CRef (Ident (loc,id),_) -> found loc id bdvars l
-    | CNotation ("{ _ : _ | _ }", ((_, CRef (Ident (_, id),_)) :: _, [], [])) when not (Id.Set.mem id bdvars) ->
-	Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l (loc, c)
-    | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l (loc, c)
+    | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) ->
+	Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+    | _ -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
 let ids_of_names l =
@@ -252,18 +252,22 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, decl) ->
     let id' = next_name_away_from (RelDecl.get_name decl) avoid in
-      (Loc.tag @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid)
+      (CAst.make @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid)
 
-let destClassApp (loc, cl) =
-  match cl with
-    | CApp ((None, (_loc, CRef (ref, inst))), l) -> Loc.tag ?loc (ref, List.map fst l, inst)
+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)
     | _ -> raise Not_found
 
-let destClassAppExpl (loc, cl) =
-  match cl with
-    | CApp ((None, (_loc, CRef (ref, inst))), l) -> Loc.tag ?loc (ref, l, inst)
+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)
     | _ -> raise Not_found
 
@@ -296,7 +300,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-	    Loc.tag ?loc @@ CAppExpl ((None, id, inst), args), avoid
+	    CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/notation.ml b/interp/notation.ml
index 150be040f..03dffa6ee 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -471,7 +471,7 @@ let interp_prim_token =
 
 (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
 
-let rec rcp_of_glob looked_for gt = Loc.map (function
+let rec rcp_of_glob looked_for gt = CAst.map_from_loc (fun ?loc -> function
   | GVar id       -> RCPatAtom (Some id)
   | GHole (_,_,_) -> RCPatAtom None
   | GRef (g,_)    -> looked_for g; RCPatCstr (g,[],[])
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a74e64172..eb89b2ef2 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -43,7 +43,7 @@ let is_constructor id =
            (Nametab.locate_extended (qualid_of_ident id)))
   with Not_found -> false
 
-let rec cases_pattern_fold_names f a pt = match snd pt with
+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,id) -> f id a
@@ -58,7 +58,7 @@ let rec cases_pattern_fold_names f a pt = match snd pt with
   | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
   | CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a
   | CPatPrim _ | CPatAtom _ -> a
-  | CPatCast ((loc,_),_) ->
+  | CPatCast ({CAst.loc},_) ->
      CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
                       (Pp.strbrk "Casts are not supported here.")
 
@@ -103,7 +103,7 @@ let rec fold_local_binders g f n acc b = function
   | [] ->
       f n acc b
 
-let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function
+let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
   | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
   | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
@@ -115,7 +115,7 @@ let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
-      List.fold_left (fun acc bl -> fold_local_binders g f n acc (Loc.tag @@ CHole (None,IntroAnonymous,None)) bl) acc bll
+      List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll
   | CGeneralization (_,_,c) -> f n acc c
   | CDelimiters (_,a) -> f n acc a
   | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
@@ -146,7 +146,7 @@ let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
-  | _loc, CRef (Ident (_,id),_) -> if Id.List.mem id bdvars then l else Id.Set.add id l
+  | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
   | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
   in aux [] Id.Set.empty c
 
@@ -210,7 +210,7 @@ let map_local_binders f g e bl =
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
-let map_constr_expr_with_binders g f e = Loc.map (function
+let map_constr_expr_with_binders g f e = CAst.map (function
   | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l)
   | CApp ((p,a),l) ->
       CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
@@ -263,8 +263,8 @@ let map_constr_expr_with_binders g f e = Loc.map (function
 
 (* Used in constrintern *)
 let rec replace_vars_constr_expr l = function
-  | loc, CRef (Ident (loc_id,id),us) as x ->
-      (try loc, CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x)
+  | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x ->
+      (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x)
   | c -> map_constr_expr_with_binders Id.Map.remove
            replace_vars_constr_expr l c