[ltac] Use CAst nodes in the tactic AST.

This provides several advantages to people serializing tactic
scripts. Appearance of the involved constructors is common enough as
to bother to submit this PR.

15 files changed, 137 insertions, 137 deletions

diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index 6388906f5e..d9338f0421 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -333,7 +333,7 @@ open Tacexpr
 let initial_atomic () =
   let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
   let iter (s, t) =
-    let body = TacAtom (Loc.tag t) in
+    let body = TacAtom (CAst.make t) in
     Tacenv.register_ltac false false (Names.Id.of_string s) body
   in
   let () = List.iter iter
@@ -348,7 +348,7 @@ let initial_atomic () =
   List.iter iter
       [ "idtac",TacId [];
         "fail", TacFail(TacLocal,ArgArg 0,[]);
-        "fresh", TacArg(Loc.tag @@ TacFreshId [])
+        "fresh", TacArg(CAst.make @@ TacFreshId [])
       ]
 
 let () = Mltop.declare_cache_obj initial_atomic "ltac_plugin"
@@ -379,8 +379,8 @@ let initial_tacticals () =
   let varn n = Reference (ArgVar (CAst.make (idn n))) in
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
   List.iter iter [
-    "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0])));
-    "solve", TacFun ([Name (idn 0)], TacML (None, (initial_entry "solve", [varn 0])));
+    "first", TacFun ([Name (idn 0)], TacML (CAst.make (initial_entry "first", [varn 0])));
+    "solve", TacFun ([Name (idn 0)], TacML (CAst.make (initial_entry "solve", [varn 0])));
   ]
 
 let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin"
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 70e5ab38bc..04a8ae1746 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -767,7 +767,7 @@ let case_eq_intros_rewrite x =
 let rec find_a_destructable_match sigma t =
   let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in
   let cl = [cl, (None, None), None], None in
-  let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in
+  let dest = TacAtom (CAst.make @@ TacInductionDestruct(false, false, cl)) in
   match EConstr.kind sigma t with
     | Case (_,_,x,_) when closed0 sigma x ->
 	if isVar sigma x then
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c58c8556c5..9730fc7fd8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -33,7 +33,7 @@ open Pltac
 let fail_default_value = Locus.ArgArg 0
 
 let arg_of_expr = function
-    TacArg (loc,a) -> a
+    TacArg { CAst.v } -> v
   | e -> Tacexp (e:raw_tactic_expr)
 
 let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
@@ -162,9 +162,9 @@ GRAMMAR EXTEND Gram
       | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ];
 	  l = LIST0 message_token -> { TacFail (g,n,l) }
       | st = simple_tactic -> { st }
-      | a = tactic_arg -> { TacArg(Loc.tag ~loc a) }
+      | a = tactic_arg -> { TacArg(CAst.make ~loc a) }
       | r = reference; la = LIST0 tactic_arg_compat ->
-        { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ]
+        { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ]
     | "0"
       [ "("; a = tactic_expr; ")" -> { a }
       | "["; ">"; tg = tactic_then_gen; "]" -> {
@@ -173,7 +173,7 @@ GRAMMAR EXTEND Gram
           | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl)
           | None -> TacDispatch tf
           end }
-      | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ]
+      | a = tactic_atom -> { TacArg (CAst.make ~loc a) } ] ]
   ;
   failkw:
   [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ]
@@ -223,7 +223,7 @@ GRAMMAR EXTEND Gram
   ;
   tactic_atom:
     [ [ n = integer -> { TacGeneric (genarg_of_int n) }
-      | r = reference -> { TacCall (Loc.tag ~loc (r,[])) }
+      | r = reference -> { TacCall (CAst.make ~loc (r,[])) }
       | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
   ;
   match_key:
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 571595be70..0ce0fbd0cd 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -529,178 +529,178 @@ GRAMMAR EXTEND Gram
     [ [
       (* Basic tactics *)
         IDENT "intros"; pl = ne_intropatterns ->
-          { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) }
+          { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,pl)) }
       | IDENT "intros" ->
-          { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
+          { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
       | IDENT "eintros"; pl = ne_intropatterns ->
-          { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) }
+          { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) }
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) }
+          inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) }
       | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) }
+          inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,true,cl,inhyp)) }
       | IDENT "simple"; IDENT "apply";
           cl = LIST1 constr_with_bindings_arg SEP ",";
-          inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,false,cl,inhyp)) }
+          inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (false,false,cl,inhyp)) }
       | IDENT "simple"; IDENT "eapply";
           cl = LIST1 constr_with_bindings_arg SEP",";
-          inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,true,cl,inhyp)) }
+          inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (false,true,cl,inhyp)) }
       | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
-          { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) }
+          { TacAtom (CAst.make ~loc @@ TacElim (false,cl,el)) }
       | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator ->
-          { TacAtom (Loc.tag ~loc @@ TacElim (true,cl,el)) }
-      | IDENT "case"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase false icl) }
-      | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase true icl) }
+          { TacAtom (CAst.make ~loc @@ TacElim (true,cl,el)) }
+      | IDENT "case"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase false icl) }
+      | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (CAst.make ~loc @@ mkTacCase true icl) }
       | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
-	  { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
+	  { TacAtom (CAst.make ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) }
       | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
-	  { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
+	  { TacAtom (CAst.make ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) }
 
       | IDENT "pose"; bl = bindings_with_parameters ->
-	  { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
+	  { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) }
       | IDENT "pose"; b = constr; na = as_name ->
-	  { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
+	  { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) }
       | IDENT "epose"; bl = bindings_with_parameters ->
-	  { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
+	  { let (id,b) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) }
       | IDENT "epose"; b = constr; na = as_name ->
-	  { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
+	  { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) }
       | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl ->
-	  { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
+	  { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) }
       | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,true,None)) }
+          { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,c,p,true,None)) }
       | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl ->
-	  { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) }
+	  { let (id,c) = bl in TacAtom (CAst.make ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) }
       | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,true,None)) }
+          { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,c,p,true,None)) }
       | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
           p = clause_dft_all ->
-          { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,false,e)) }
+          { TacAtom (CAst.make ~loc @@ TacLetTac (false,na,c,p,false,e)) }
       | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
           p = clause_dft_all ->
-          { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,false,e)) }
+          { TacAtom (CAst.make ~loc @@ TacLetTac (true,na,c,p,false,e)) }
 
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
 	  c = lconstr; ")" ->
           { let { CAst.loc = loc; v = id } = lid in
-          TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+          TacAtom (CAst.make ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
       | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":=";
 	  c = lconstr; ")" ->
           { let { CAst.loc = loc; v = id } = lid in
-          TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+          TacAtom (CAst.make ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
 
       (* Alternative syntax for "assert c as id by tac" *)
       | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
           { let { CAst.loc = loc; v = id } = lid in
-          TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+          TacAtom (CAst.make ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
       | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
           { let { CAst.loc = loc; v = id } = lid in
-          TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+          TacAtom (CAst.make ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
 
       (* Alternative syntax for "enough c as id by tac" *)
       | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
           { let { CAst.loc = loc; v = id } = lid in
-          TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+          TacAtom (CAst.make ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
       | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
           { let { CAst.loc = loc; v = id } = lid in
-          TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
+          TacAtom (CAst.make ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) }
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
+	  { TacAtom (CAst.make ~loc @@ TacAssert (false,true,Some tac,ipat,c)) }
       | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
+	  { TacAtom (CAst.make ~loc @@ TacAssert (true,true,Some tac,ipat,c)) }
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) }
+	  { TacAtom (CAst.make ~loc @@ TacAssert (false,true,None,ipat,c)) }
       | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) }
+	  { TacAtom (CAst.make ~loc @@ TacAssert (true,true,None,ipat,c)) }
       | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
+	  { TacAtom (CAst.make ~loc @@ TacAssert (false,false,Some tac,ipat,c)) }
       | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
+	  { TacAtom (CAst.make ~loc @@ TacAssert (true,false,Some tac,ipat,c)) }
 
       | IDENT "generalize"; c = constr ->
-	  { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
+	  { TacAtom (CAst.make ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) }
       | IDENT "generalize"; c = constr; l = LIST1 constr ->
 	  { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
-          TacAtom (Loc.tag ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) }
+          TacAtom (CAst.make ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) }
       | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
           na = as_name;
           l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] ->
-          { TacAtom (Loc.tag ~loc @@ TacGeneralize (((nl,c),na)::l)) }
+          { TacAtom (CAst.make ~loc @@ TacGeneralize (((nl,c),na)::l)) }
 
       (* Derived basic tactics *)
       | IDENT "induction"; ic = induction_clause_list ->
-	  { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) }
+	  { TacAtom (CAst.make ~loc @@ TacInductionDestruct (true,false,ic)) }
       | IDENT "einduction"; ic = induction_clause_list ->
-	  { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) }
+	  { TacAtom (CAst.make ~loc @@ TacInductionDestruct(true,true,ic)) }
       | IDENT "destruct"; icl = induction_clause_list ->
-	  { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) }
+	  { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,false,icl)) }
       | IDENT "edestruct";  icl = induction_clause_list ->
-	  { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) }
+	  { TacAtom (CAst.make ~loc @@ TacInductionDestruct(false,true,icl)) }
 
       (* Equality and inversion *)
       | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (false,l,cl,t)) }
+	  cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (false,l,cl,t)) }
       | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ",";
-	  cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) }
+	  cl = clause_dft_concl; t=by_tactic -> { TacAtom (CAst.make ~loc @@ TacRewrite (true,l,cl,t)) }
       | IDENT "dependent"; k =
 	  [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion }
 	  | IDENT "inversion" -> { FullInversion }
 	  | IDENT "inversion_clear" -> { FullInversionClear } ];
 	  hyp = quantified_hypothesis;
 	  ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] ->
-	    { TacAtom (Loc.tag ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) }
+	    { TacAtom (CAst.make ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) }
       | IDENT "simple"; IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = as_or_and_ipat;
 	  cl = in_hyp_list ->
-	    { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
+	    { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) }
       | IDENT "inversion";
 	  hyp = quantified_hypothesis; ids = as_or_and_ipat;
 	  cl = in_hyp_list ->
-	    { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
+	    { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) }
       | IDENT "inversion_clear";
 	  hyp = quantified_hypothesis; ids = as_or_and_ipat;
 	  cl = in_hyp_list ->
-	    { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
+	    { TacAtom (CAst.make ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) }
       | IDENT "inversion"; hyp = quantified_hypothesis;
 	  "using"; c = constr; cl = in_hyp_list ->
-	    { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
+	    { TacAtom (CAst.make ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) }
 
       (* Conversion *)
       | IDENT "red"; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Red false, cl)) }
       | IDENT "hnf"; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Hnf, cl)) }
       | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Simpl (all_with d, po), cl)) }
       | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Cbv s, cl)) }
       | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Cbn s, cl)) }
       | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Lazy s, cl)) }
       | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Cbv (all_with delta), cl)) }
       | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (CbvVm po, cl)) }
       | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (CbvNative po, cl)) }
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Unfold ul, cl)) }
       | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Fold l, cl)) }
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl ->
-          { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) }
+          { TacAtom (CAst.make ~loc @@ TacReduce (Pattern pl, cl)) }
 
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "change"; c = conversion; cl = clause_dft_concl ->
 	  { let (oc, c) = c in
 	  let p,cl = merge_occurrences loc cl oc in
-	  TacAtom (Loc.tag ~loc @@ TacChange (p,c,cl)) }
+	  TacAtom (CAst.make ~loc @@ TacChange (p,c,cl)) }
     ] ]
   ;
 END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b219ee25ca..50cfb6d004 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -294,7 +294,7 @@ let string_of_genarg_arg (ArgumentType arg) =
       let pr _ = str "_" in
       KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
 
-  let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg))
+  let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg))
 
   let is_genarg tag wit =
     let ArgT.Any tag = tag in
@@ -350,9 +350,9 @@ let string_of_genarg_arg (ArgumentType arg) =
     pr_extend_gen (pr_farg prtac)
 
   let pr_raw_alias prtac lev key args =
-    pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
+    pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args
   let pr_glob_alias prtac lev key args =
-    pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
+    pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (CAst.make a)))) lev key args
 
   (**********************************************************************)
   (* The tactic printer                                                 *)
@@ -579,7 +579,7 @@ let pr_goal_selector ~toplevel s =
            pr_gen  arg
          else
            str name ++ str ":" ++ surround (pr_gen arg)
-      | _ -> pr_arg (TacArg (Loc.tag t)) in
+      | _ -> pr_arg (TacArg (CAst.make t)) in
     hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++
              str " :=" ++ brk (1,1) ++ pr t)
 
@@ -1045,30 +1045,30 @@ let pr_goal_selector ~toplevel s =
             | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
-            | TacAtom (loc,t) ->
+            | TacAtom { CAst.loc; v=t } ->
               pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
-            | TacArg(_,Tacexp e) ->
+            | TacArg { CAst.v=Tacexp e } ->
               pr_tac inherited e, latom
-            | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
+            | TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } ->
               keyword "constr:" ++ pr.pr_constr c, latom
-            | TacArg(_,ConstrMayEval c) ->
+            | TacArg { CAst.v=ConstrMayEval c } ->
               pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
-            | TacArg(_,TacFreshId l) ->
+            | TacArg { CAst.v=TacFreshId l } ->
               primitive "fresh" ++ pr_fresh_ids l, latom
-            | TacArg(_,TacGeneric arg) ->
+            | TacArg { CAst.v=TacGeneric arg } ->
               pr.pr_generic arg, latom
-            | TacArg(_,TacCall(_,(f,[]))) ->
+            | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
               pr.pr_reference f, latom
-            | TacArg(_,TacCall(loc,(f,l))) ->
+            | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
               pr_with_comments ?loc (hov 1 (
                 pr.pr_reference f ++ spc ()
                 ++ prlist_with_sep spc pr_tacarg l)),
               lcall
-            | TacArg (_,a) ->
+            | TacArg { CAst.v=a } ->
               pr_tacarg a, latom
-            | TacML (loc,(s,l)) ->
+            | TacML { CAst.loc; v=(s,l) } ->
               pr_with_comments ?loc (pr.pr_extend 1 s l), lcall
-            | TacAlias (loc,(kn,l)) ->
+            | TacAlias { CAst.loc; v=(kn,l) } ->
               pr_with_comments ?loc (pr.pr_alias (level_of inherited) kn l), latom
           )
           in
@@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s =
           | TacNumgoals ->
             keyword "numgoals"
           | (TacCall _|Tacexp _ | TacGeneric _) as a ->
-            hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.tag a))))
+            hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (CAst.make a))))
 
         in pr_tac
 
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index db7dcfa6ef..3eb049dbab 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -251,7 +251,7 @@ let string_of_call ck =
        | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id
        | Tacexpr.LtacAtomCall te ->
          (Pptactic.pr_glob_tactic (Global.env ())
-            (Tacexpr.TacAtom (Loc.tag te)))
+            (Tacexpr.TacAtom (CAst.make te)))
        | Tacexpr.LtacConstrInterp (c, _) ->
          pr_glob_constr_env (Global.env ()) c
        | Tacexpr.LtacMLCall te ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 7d917c58fe..16cb75ea2f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1958,7 +1958,7 @@ let add_setoid atts binders a aeq t n =
 let make_tactic name =
   let open Tacexpr in
   let tacqid = Libnames.qualid_of_string name in
-  TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, []))))
+  TacArg (CAst.make @@ (TacCall (CAst.make (tacqid, []))))
 
 let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 1b212334ce..188d5de7de 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -177,7 +177,7 @@ let add_tactic_entry (kn, ml, tg) state =
         TacGeneric arg
     in
     let l = List.map map l in
-    (TacAlias (Loc.tag ~loc (kn,l)):raw_tactic_expr)
+    (TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr)
   in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
@@ -349,7 +349,7 @@ let extend_atomic_tactic name entries =
     | TacNonTerm (_, (symb, _)) ->
       let EntryName (typ, e) = prod_item_of_symbol 0 symb in
       let Genarg.Rawwit wit = typ in
-      let inj x = TacArg (Loc.tag @@ TacGeneric (Genarg.in_gen typ x)) in
+      let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in
       let default = epsilon_value inj e in
       match default with
       | None -> raise NonEmptyArgument
@@ -363,7 +363,7 @@ let extend_atomic_tactic name entries =
   | Some (id, args) ->
     let args = List.map (fun a -> Tacexp a) args in
     let entry = { mltac_name = name; mltac_index = i } in
-    let body = TacML (Loc.tag (entry, args)) in
+    let body = TacML (CAst.make (entry, args)) in
     Tacenv.register_ltac false false (Names.Id.of_string id) body
   in
   List.iteri add_atomic entries
@@ -379,7 +379,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods =
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Locus.ArgVar (CAst.make id)) in
-    let tac = TacML (Loc.tag (entry, List.map map ids)) in
+    let tac = TacML (CAst.make (entry, List.map map ids)) in
     add_glob_tactic_notation false ~level ?deprecation prods true ids tac
   in
   List.iteri iter (List.rev prods);
@@ -664,7 +664,7 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign =
   (** Arguments are not passed directly to the ML tactic in the TacML node,
       the ML tactic retrieves its arguments in the [ist] environment instead.
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
-    let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
+    let body = Tacexpr.TacFun (vars, Tacexpr.TacML (CAst.make (ml, [])))in
     let id = Names.Id.of_string name in
     let obj () = Tacenv.register_ltac true false id body ?deprecation in
     let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 8731cbf60d..9435d0b911 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -167,7 +167,7 @@ type 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
   | Reference      of 'ref
-  | TacCall    of ('ref * 'a gen_tactic_arg list) Loc.located
+  | TacCall    of ('ref * 'a gen_tactic_arg list) CAst.t
   | TacFreshId of string or_var list
   | Tacexp of 'tacexpr
   | TacPretype of 'trm
@@ -189,7 +189,7 @@ constraint 'a = <
     'r : ltac refs, 'n : idents, 'l : levels *)
 
 and 'a gen_tactic_expr =
-  | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
+  | TacAtom of ('a gen_atomic_tactic_expr) CAst.t
   | TacThen of
       'a gen_tactic_expr *
       'a gen_tactic_expr
@@ -245,12 +245,12 @@ and 'a gen_tactic_expr =
   | TacMatchGoal of lazy_flag * direction_flag *
       ('p,'a gen_tactic_expr) match_rule list
   | TacFun of 'a gen_tactic_fun_ast
-  | TacArg of 'a gen_tactic_arg located
+  | TacArg of 'a gen_tactic_arg CAst.t
   | TacSelect of Goal_select.t * 'a gen_tactic_expr
   (* For ML extensions *)
-  | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
+  | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) CAst.t
   (* For syntax extensions *)
-  | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
+  | TacAlias of (KerName.t * 'a gen_tactic_arg list) CAst.t
 
 constraint 'a = <
     term:'t;
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9958d6dcda..1527724420 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -167,7 +167,7 @@ type 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
   | Reference      of 'ref
-  | TacCall    of ('ref * 'a gen_tactic_arg list) Loc.located
+  | TacCall    of ('ref * 'a gen_tactic_arg list) CAst.t
   | TacFreshId of string or_var list
   | Tacexp of 'tacexpr
   | TacPretype of 'trm
@@ -189,7 +189,7 @@ constraint 'a = <
     'r : ltac refs, 'n : idents, 'l : levels *)
 
 and 'a gen_tactic_expr =
-  | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
+  | TacAtom of ('a gen_atomic_tactic_expr) CAst.t
   | TacThen of
       'a gen_tactic_expr *
       'a gen_tactic_expr
@@ -245,12 +245,12 @@ and 'a gen_tactic_expr =
   | TacMatchGoal of lazy_flag * direction_flag *
       ('p,'a gen_tactic_expr) match_rule list
   | TacFun of 'a gen_tactic_fun_ast
-  | TacArg of 'a gen_tactic_arg located
+  | TacArg of 'a gen_tactic_arg CAst.t
   | TacSelect of Goal_select.t * 'a gen_tactic_expr
   (* For ML extensions *)
-  | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
+  | TacML of (ml_tactic_entry * 'a gen_tactic_arg list) CAst.t
   (* For syntax extensions *)
-  | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
+  | TacAlias of (KerName.t * 'a gen_tactic_arg list) CAst.t
 
 constraint 'a = <
     term:'t;
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ebec3c887c..85c6348b52 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -137,7 +137,7 @@ let intern_isolated_global_tactic_reference qid =
   let kn = Tacenv.locate_tactic qid in
   Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
     Tacenv.tac_deprecation kn;
-  TacCall (Loc.tag ?loc (ArgArg (loc,kn),[]))
+  TacCall (CAst.make ?loc (ArgArg (loc,kn),[]))
 
 let intern_isolated_tactic_reference strict ist qid =
   (* An ltac reference *)
@@ -587,10 +587,10 @@ let rec intern_atomic lf ist x =
 and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
 
 and intern_tactic_seq onlytac ist = function
-  | TacAtom (loc,t) ->
+  | TacAtom { loc; v=t } ->
       let lf = ref ist.ltacvars in
       let t = intern_atomic lf ist t in
-      !lf, TacAtom (Loc.tag ?loc:(adjust_loc loc) t)
+      !lf, TacAtom (CAst.make ?loc:(adjust_loc loc) t)
   | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
   | TacLetIn (isrec,l,u) ->
       let ltacvars = Id.Set.union (extract_let_names l) ist.ltacvars in
@@ -659,27 +659,27 @@ and intern_tactic_seq onlytac ist = function
   | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l)
   | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
   | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
-  | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+  | TacArg { loc; v=a } -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
   | TacSelect (sel, tac) ->
       ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac)
 
   (* For extensions *)
-  | TacAlias (loc,(s,l)) ->
+  | TacAlias { loc; v=(s,l) } ->
       let alias = Tacenv.interp_alias s in
       Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation;
       let l = List.map (intern_tacarg !strict_check false ist) l in
-      ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
-  | TacML (loc,(opn,l)) ->
+      ist.ltacvars, TacAlias (CAst.make ?loc (s,l))
+  | TacML { loc; v=(opn,l) } ->
       let _ignore = Tacenv.interp_ml_tactic opn in
-      ist.ltacvars, TacML (loc, (opn,List.map (intern_tacarg !strict_check false ist) l))
+      ist.ltacvars, TacML CAst.(make ?loc (opn,List.map (intern_tacarg !strict_check false ist) l))
 
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
   | TacCall _ | Reference _
-  | TacGeneric _ as a -> TacArg (loc,a)
+  | TacGeneric _ as a -> TacArg CAst.(make ?loc a)
   | Tacexp a -> a
   | ConstrMayEval _ | TacFreshId _ | TacPretype _ | TacNumgoals as a ->
-      if onlytac then error_tactic_expected ?loc else TacArg (loc,a)
+      if onlytac then error_tactic_expected ?loc else TacArg CAst.(make ?loc a)
 
 and intern_tactic_or_tacarg ist = intern_tactic false ist
 
@@ -692,9 +692,9 @@ and intern_tactic_fun ist (var,body) =
 and intern_tacarg strict onlytac ist = function
   | Reference r -> intern_non_tactic_reference strict ist r
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
-  | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f
-  | TacCall (loc,(f,l)) ->
-      TacCall (Loc.tag ?loc (
+  | TacCall { loc; v=(f,[]) } -> intern_isolated_tactic_reference strict ist f
+  | TacCall { loc; v=(f,l) } ->
+      TacCall (CAst.make ?loc (
         intern_applied_tactic_reference ist f,
         List.map (intern_tacarg !strict_check false ist) l))
   | TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5bfb0f79fb..cb3a0aaed9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1018,7 +1018,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
   | TacLetIn (false,l,u) -> interp_letin ist l u
   | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
   | TacMatch (lz,c,lmr) -> interp_match ist lz c lmr
-  | TacArg (loc,a) -> interp_tacarg ist a
+  | TacArg {loc;v} -> interp_tacarg ist v
   | t ->
     (** Delayed evaluation *)
     Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
@@ -1036,7 +1036,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
 
 
 and eval_tactic ist tac : unit Proofview.tactic = match tac with
-  | TacAtom (loc,t) ->
+  | TacAtom {loc;v=t} ->
       let call = LtacAtomCall t in
       push_trace(loc,call) ist >>= fun trace ->
       Profile_ltac.do_profile "eval_tactic:2" trace
@@ -1116,7 +1116,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       eval_tactic ist tac
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
-  | TacAlias (loc,(s,l)) ->
+  | TacAlias {loc; v=(s,l)} ->
       let alias = Tacenv.interp_alias s in
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
@@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       in
       Ftactic.run tac (fun () -> Proofview.tclUNIT ())
 
-  | TacML (loc,(opn,l)) ->
+  | TacML {loc; v=(opn,l)} ->
       push_trace (Loc.tag ?loc @@ LtacMLCall tac) ist >>= fun trace ->
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       let tac = Tacenv.interp_ml_tactic opn in
@@ -1201,9 +1201,9 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
         Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
         (Ftactic.return (Value.of_constr c_interp))
       end
-  | TacCall (loc,(r,[])) ->
+  | TacCall { v=(r,[]) } ->
       interp_ltac_reference true ist r
-  | TacCall (loc,(f,l)) ->
+  | TacCall { loc; v=(f,l) } ->
       let (>>=) = Ftactic.bind in
       interp_ltac_reference true ist f >>= fun fv ->
       Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
@@ -1337,7 +1337,7 @@ and interp_letrec ist llc u =
   Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *)
   let lref = ref ist.lfun in
   let fold accu ({v=na}, b) =
-    let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in
+    let v = of_tacvalue (VRec (lref, TacArg (CAst.make b))) in
     Name.fold_right (fun id -> Id.Map.add id v) na accu
   in
   let lfun = List.fold_left fold ist.lfun llc in
@@ -1875,7 +1875,7 @@ module Value = struct
     let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
     let lfun = Id.Map.add (Id.of_string "F") f lfun in
     let ist = { (default_ist ()) with lfun = lfun; } in
-    let tac = TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+    let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
     eval_tactic_ist ist tac
 
 end
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 9173e23b89..caaa547a07 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -173,7 +173,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
 
 and subst_tactic subst (t:glob_tactic_expr) = match t with
-  | TacAtom (_loc,t) -> TacAtom (Loc.tag @@ subst_atomic subst t)
+  | TacAtom { CAst.v=t } -> TacAtom (CAst.make @@ subst_atomic subst t)
   | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
   | TacLetIn (r,l,u) ->
       let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
@@ -220,22 +220,22 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
   | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
   | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
   | TacComplete tac -> TacComplete (subst_tactic subst tac)
-  | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a)
+  | TacArg { CAst.v=a } -> TacArg (CAst.make @@ subst_tacarg subst a)
   | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac)
 
   (* For extensions *)
-  | TacAlias (_,(s,l)) ->
+  | TacAlias { CAst.v=(s,l) } ->
       let s = subst_kn subst s in
-      TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l))
-  | TacML (loc,(opn,l)) -> TacML (loc, (opn,List.map (subst_tacarg subst) l))
+      TacAlias (CAst.make (s,List.map (subst_tacarg subst) l))
+  | TacML { CAst.loc; v=(opn,l)} -> TacML CAst.(make ?loc (opn,List.map (subst_tacarg subst) l))
 
 and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 
 and subst_tacarg subst = function
   | Reference r -> Reference (subst_reference subst r)
   | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
-  | TacCall (loc,(f,l)) ->
-      TacCall (Loc.tag ?loc (subst_reference subst f, List.map (subst_tacarg subst) l))
+  | TacCall { CAst.loc; v=(f,l) } ->
+      TacCall CAst.(make ?loc (subst_reference subst f, List.map (subst_tacarg subst) l))
   | TacFreshId _ as x -> x
   | TacPretype c -> TacPretype (subst_glob_constr subst c)
   | TacNumgoals -> TacNumgoals
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 6bab8d0353..877d4ee758 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -365,7 +365,7 @@ let explain_ltac_call_trace last trace loc =
         Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
   | Tacexpr.LtacAtomCall te ->
       quote (Pptactic.pr_glob_tactic (Global.env())
-              (Tacexpr.TacAtom (Loc.tag te)))
+              (Tacexpr.TacAtom (CAst.make te)))
   | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) ->
       quote (Printer.pr_glob_constr_env (Global.env()) c) ++
         (if not (Id.Map.is_empty vars) then
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 299bc7ea4d..561bfc5d7c 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -191,7 +191,7 @@ let make_unfold name =
 let u_not = make_unfold "not"
 
 let reduction_not_iff _ ist =
-  let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
+  let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
   let tac = match !negation_unfolding with
     | true -> make_reduce [u_not]
     | false -> TacId []
@@ -244,7 +244,7 @@ let with_flags flags _ ist =
   let x = CAst.make @@ Id.of_string "x" in
   let arg = Val.Dyn (tag_tauto_flags, flags) in
   let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
-  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
+  eval_tactic_ist ist (TacArg (CAst.make @@ TacCall (CAst.make (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
 
 let register_tauto_tactic tac name0 args =
   let ids = List.map (fun id -> Id.of_string id) args in
@@ -252,7 +252,7 @@ let register_tauto_tactic tac name0 args =
   let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in
   let entry = { mltac_name = name; mltac_index = 0 } in
   let () = Tacenv.register_ml_tactic name [| tac |] in
-  let tac = TacFun (ids, TacML (Loc.tag (entry, []))) in
+  let tac = TacFun (ids, TacML (CAst.make (entry, []))) in
   let obj () = Tacenv.register_ltac true true (Id.of_string name0) tac in
   Mltop.declare_cache_obj obj tauto_plugin