[located] More work towards using CAst.t

We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:

- module declarations
- intro patterns
- top-level sentences

Now, parsed documents should be full annotated by `CAst` nodes.

10 files changed, 124 insertions, 123 deletions

diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 61632e388..2e90ce90c 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -264,7 +264,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
 	  (Declare.declare_universe_context false ctx;
            Univ.ContextSet.empty)
     in
-      Loc.tag ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
+      CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
   let eqs = List.map f lcsr in
   let add_hints base = add_rew_rules base eqs in
   List.iter add_hints bases
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 66268f9f9..1909cd96f 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -198,7 +198,8 @@ GEXTEND Gram
      verbose most of the time. *)
   fresh_id:
     [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
-        | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ]
+        | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
+                          ArgVar (CAst.make ~loc:!@loc id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1b8a852d9..7643cc97d 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -175,7 +175,7 @@ let mkCLambdaN_simple bl c = match bl with
     let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in
     mkCLambdaN_simple_loc ?loc bl c
 
-let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
+let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc
 
 let map_int_or_var f = function
   | ArgArg x -> ArgArg (f x)
@@ -297,7 +297,7 @@ GEXTEND Gram
 	  (* (A & B & C) is translated into (A,(B,C)) *)
 	  let rec pairify = function
 	    | ([]|[_]|[_;_]) as l -> l
-	    | t::q -> [t; Loc.tag ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
+            | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))]
 	  in IntroAndPattern (pairify (si::tc)) ] ]
   ;
   equality_intropattern:
@@ -312,28 +312,28 @@ GEXTEND Gram
   ;
   nonsimple_intropattern:
     [ [ l = simple_intropattern -> l
-      | "*"  -> Loc.tag ~loc:!@loc @@ IntroForthcoming true
-      | "**" -> Loc.tag ~loc:!@loc @@ IntroForthcoming false ]]
+      | "*"  -> CAst.make ~loc:!@loc @@ IntroForthcoming true
+      | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]]
   ;
   simple_intropattern:
     [ [ pat = simple_intropattern_closed;
         l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
-          let loc0,pat = pat in
+          let {CAst.loc=loc0;v=pat} = pat in
           let f c pat =
             let loc1 = Constrexpr_ops.constr_loc c in
             let loc = Loc.merge_opt loc0 loc1 in
-            IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
-          Loc.tag ~loc:!@loc @@ List.fold_right f l pat ] ]
+            IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in
+          CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ]
   ;
   simple_intropattern_closed:
-    [ [ pat = or_and_intropattern   -> Loc.tag ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat)
-      | pat = equality_intropattern -> Loc.tag ~loc:!@loc @@ IntroAction pat
-      | "_" -> Loc.tag ~loc:!@loc @@ IntroAction IntroWildcard 
-      | pat = naming_intropattern -> Loc.tag ~loc:!@loc @@ IntroNaming pat ] ]
+    [ [ pat = or_and_intropattern   -> CAst.make ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat)
+      | pat = equality_intropattern -> CAst.make ~loc:!@loc @@ IntroAction pat
+      | "_" -> CAst.make ~loc:!@loc @@ IntroAction IntroWildcard
+      | pat = naming_intropattern -> CAst.make ~loc:!@loc @@ IntroNaming pat ] ]
   ;
   simple_binding:
-    [ [ "("; id = ident; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (NamedHyp id, c)
-      | "("; n = natural; ":="; c = lconstr; ")" -> Loc.tag ~loc:!@loc (AnonHyp n, c) ] ]
+    [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c)
+      | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ]
   ;
   bindings:
     [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
@@ -470,7 +470,7 @@ GEXTEND Gram
       | -> None ] ]
   ;
   or_and_intropattern_loc:
-    [ [ ipat = or_and_intropattern -> ArgArg (Loc.tag ~loc:!@loc ipat)
+    [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat)
       | locid = identref -> ArgVar locid ] ]
   ;
   as_or_and_ipat:
@@ -478,13 +478,13 @@ GEXTEND Gram
       | -> None ] ]
   ;
   eqn_ipat:
-    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (Loc.tag ~loc:!@loc pat)
+    [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat)
       | IDENT "_eqn"; ":"; pat = naming_intropattern ->
          let loc = !@loc in
-	 warn_deprecated_eqn_syntax ~loc "H"; Some (Loc.tag ~loc pat)
+         warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat)
       | IDENT "_eqn" ->
          let loc = !@loc in
-	 warn_deprecated_eqn_syntax ~loc "?"; Some (Loc.tag ~loc IntroAnonymous)
+         warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous)
       | -> None ] ]
   ;
   as_name:
@@ -525,7 +525,7 @@ GEXTEND Gram
         IDENT "intros"; pl = ne_intropatterns ->
           TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl))
       | IDENT "intros" ->
-          TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[Loc.tag ~loc:!@loc @@IntroForthcoming false]))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false]))
       | IDENT "eintros"; pl = ne_intropatterns ->
           TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl))
 
@@ -577,31 +577,31 @@ GEXTEND Gram
       | 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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+          TacAtom (Loc.tag ?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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+          TacAtom (Loc.tag ?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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+          TacAtom (Loc.tag ?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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+          TacAtom (Loc.tag ?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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+          TacAtom (Loc.tag ?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 (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c))
+          TacAtom (Loc.tag ?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:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 699e23110..6637de745 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -10,7 +10,6 @@
 
 (** Ltac parsing entries *)
 
-open Loc
 open Pcoq
 open Libnames
 open Constrexpr
@@ -29,7 +28,7 @@ val quantified_hypothesis : quantified_hypothesis Gram.entry
 val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
 val int_or_var : int or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
-val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry
+val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
 val in_clause : lident Locus.clause_expr Gram.entry
 val clause_dft_concl : lident Locus.clause_expr Gram.entry
 val tactic_arg : raw_tactic_arg Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fbb70cca6..a42994652 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -183,7 +183,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_or_by_notation f = function
     | AN v -> f v
-    | ByNotation (_,(s,sc)) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+    | ByNotation {CAst.v=(s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
   let pr_located pr (loc,x) = pr x
 
@@ -382,9 +382,9 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_as_disjunctive_ipat prc ipatl =
     keyword "as" ++ spc () ++
-      pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
+      pr_or_var (fun {CAst.loc;v=p} -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
 
-  let pr_eqn_ipat (_,ipat) = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
+  let pr_eqn_ipat {CAst.v=ipat} = keyword "eqn:" ++ Miscprint.pr_intro_pattern_naming ipat
 
   let pr_with_induction_names prc = function
     | None, None -> mt ()
@@ -426,7 +426,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_assumption prc prdc prlc ipat c = match ipat with
     (* Use this "optimisation" or use only the general case ?*)
     (* it seems that this "optimisation" is somehow more natural *)
-    | Some (_,IntroNaming (IntroIdentifier id)) ->
+    | Some {CAst.v=IntroNaming (IntroIdentifier id)} ->
       spc() ++ surround (pr_id id ++ str " :" ++ spc() ++ prlc c)
     | ipat ->
       spc() ++ prc c ++ pr_as_ipat prdc ipat
@@ -744,7 +744,7 @@ let pr_goal_selector ~toplevel s =
         | TacIntroPattern (ev,(_::_ as p)) ->
            hov 1 (primitive (if ev then "eintros" else "intros") ++
                     (match p with
-                    | [_,Misctypes.IntroForthcoming false] -> mt ()
+                    | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt ()
                     | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 2c7ebb745..3812a2ba2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -147,7 +147,7 @@ let coerce_var_to_ident fresh env sigma v =
   let fail () = raise (CannotCoerceTo "a fresh identifier") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroNaming (IntroIdentifier id) -> id
+    | { CAst.v=IntroNaming (IntroIdentifier id)} -> id
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
     out_gen (topwit wit_var) v
@@ -171,7 +171,7 @@ let id_of_name = function
   let fail () = raise (CannotCoerceTo "an identifier") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroNaming (IntroIdentifier id) -> id
+    | {CAst.v=IntroNaming (IntroIdentifier id)} -> id
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
     out_gen (topwit wit_var) v
@@ -207,7 +207,7 @@ let id_of_name = function
 
 let coerce_to_intro_pattern env sigma v =
   if has_type v (topwit wit_intro_pattern) then
-    snd (out_gen (topwit wit_intro_pattern) v)
+    (out_gen (topwit wit_intro_pattern) v).CAst.v
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
     IntroNaming (IntroIdentifier id)
@@ -226,7 +226,7 @@ let coerce_to_intro_pattern_naming env sigma v =
 let coerce_to_hint_base v =
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroNaming (IntroIdentifier id) -> Id.to_string id
+    | {CAst.v=IntroNaming (IntroIdentifier id)} -> Id.to_string id
     | _ -> raise (CannotCoerceTo "a hint base name")
   else raise (CannotCoerceTo "a hint base name")
 
@@ -239,7 +239,7 @@ let coerce_to_constr env v =
   let fail () = raise (CannotCoerceTo "a term") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroNaming (IntroIdentifier id) ->
+    | {CAst.v=IntroNaming (IntroIdentifier id)} ->
       (try ([], constr_of_id env id) with Not_found -> fail ())
     | _ -> fail ()
   else if has_type v (topwit wit_constr) then
@@ -268,7 +268,7 @@ let coerce_to_evaluable_ref env sigma v =
   let ev =
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id
+    | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> EvalVarRef id
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
@@ -300,14 +300,14 @@ let coerce_to_intro_pattern_list ?loc env sigma v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
-    let map v = Loc.tag ?loc @@ coerce_to_intro_pattern env sigma v in
+    let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in
     List.map map l
 
 let coerce_to_hyp env sigma v =
   let fail () = raise (CannotCoerceTo "a variable") in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id
+    | {CAst.v=IntroNaming (IntroIdentifier id)} when is_variable env id -> id
     | _ -> fail ()
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
@@ -340,7 +340,7 @@ let coerce_to_quantified_hypothesis sigma v =
   if has_type v (topwit wit_intro_pattern) then
     let v = out_gen (topwit wit_intro_pattern) v in
     match v with
-    | _, IntroNaming (IntroIdentifier id) -> NamedHyp id
+    | {CAst.v=IntroNaming (IntroIdentifier id)} -> NamedHyp id
     | _ -> raise (CannotCoerceTo "a quantified hypothesis")
   else if has_type v (topwit wit_var) then
     let id = out_gen (topwit wit_var) v in
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 6db808dd6..8b0c44041 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -56,9 +56,9 @@ type inversion_kind = Misctypes.inversion_kind =
 
 type ('c,'d,'id) inversion_strength =
   | NonDepInversion of
-      inversion_kind * 'id list * 'd or_and_intro_pattern_expr located or_var option
+      inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
   | DepInversion of
-      inversion_kind * 'c option * 'd or_and_intro_pattern_expr located or_var option
+      inversion_kind * 'c option * 'd or_and_intro_pattern_expr CAst.t or_var option
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -70,8 +70,8 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings destruction_arg *
-    (intro_pattern_naming_expr located option (* eqn:... *)
-    * 'dconstr or_and_intro_pattern_expr located or_var option) (* as ... *)
+    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
 type ('constr,'dconstr,'id) induction_clause_list =
@@ -126,28 +126,28 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op
 
 type delayed_open_constr = EConstr.constr delayed_open
 
-type intro_pattern = delayed_open_constr intro_pattern_expr located
-type intro_patterns = delayed_open_constr intro_pattern_expr located list
-type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
-type intro_pattern_naming = intro_pattern_naming_expr located
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
 type 'a gen_atomic_tactic_expr =
   (* Basic tactics *)
-  | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr located list
+  | TacIntroPattern of evars_flag * 'dtrm intro_pattern_expr CAst.t list
   | TacApply of advanced_flag * evars_flag * 'trm with_bindings_arg list *
-      ('nam * 'dtrm intro_pattern_expr located option) option
+      ('nam * 'dtrm intro_pattern_expr CAst.t option) option
   | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option
   | TacCase of evars_flag * 'trm with_bindings_arg
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
       evars_flag * bool * 'tacexpr option option *
-      'dtrm intro_pattern_expr located option * 'trm
+      'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr located option
+      intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 121075f72..45f4a45fc 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -93,7 +93,7 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 
 let intern_global_reference ist = function
   | Ident (loc,id) when find_var id ist ->
-    ArgVar CAst.(make ?loc id)
+    ArgVar (make ?loc id)
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       try ArgArg (loc,locate_global_with_alias lqid)
@@ -103,20 +103,20 @@ let intern_ltac_variable ist = function
   | Ident (loc,id) ->
       if find_var id ist then
 	(* A local variable of any type *)
-        ArgVar CAst.(make ?loc id)
+        ArgVar (make ?loc id)
       else raise Not_found
   | _ ->
       raise Not_found
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
+      (DAst.make @@ GVar id), Some (make @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+      (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       DAst.make @@ GRef (locate_global_with_alias lqid,None), 
-	if strict then None else Some (CAst.make @@ CRef (r,None))
+        if strict then None else Some (make @@ CRef (r,None))
 
 (* Internalize an isolated reference in position of tactic *)
 
@@ -168,7 +168,7 @@ let intern_non_tactic_reference strict ist r =
   (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
   match r with
   | Ident (loc,id) when not strict ->
-    let ipat = in_gen (glbwit wit_intro_pattern) (loc, IntroNaming (IntroIdentifier id)) in
+    let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in
     TacGeneric ipat
   | _ ->
   (* Reference not found *)
@@ -209,8 +209,8 @@ let intern_constr = intern_constr_gen false false
 let intern_type = intern_constr_gen false true
 
 (* Globalize bindings *)
-let intern_binding ist (loc,(b,c)) =
-  (loc,(intern_binding_name ist b,intern_constr ist c))
+let intern_binding ist = map (fun (b,c) ->
+    intern_binding_name ist b,intern_constr ist c)
 
 let intern_bindings ist = function
   | NoBindings -> NoBindings
@@ -223,12 +223,12 @@ let intern_constr_with_bindings ist (c,bl) =
 let intern_constr_with_bindings_arg ist (clear,c) =
   (clear,intern_constr_with_bindings ist c)
 
-let rec intern_intro_pattern lf ist = function
-  | loc, IntroNaming pat ->
-      loc, IntroNaming (intern_intro_pattern_naming lf ist pat)
-  | loc, IntroAction pat ->
-      loc, IntroAction (intern_intro_pattern_action lf ist pat)
-  | loc, IntroForthcoming _ as x -> x
+let rec intern_intro_pattern lf ist = map (function
+  | IntroNaming pat ->
+    IntroNaming (intern_intro_pattern_naming lf ist pat)
+  | IntroAction pat ->
+    IntroAction (intern_intro_pattern_action lf ist pat)
+  | IntroForthcoming _ as x -> x)
 
 and intern_intro_pattern_naming lf ist = function
   | IntroIdentifier id ->
@@ -239,12 +239,12 @@ and intern_intro_pattern_naming lf ist = function
 
 and intern_intro_pattern_action lf ist = function
   | IntroOrAndPattern l ->
-      IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+    IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
   | IntroInjection l ->
-      IntroInjection (List.map (intern_intro_pattern lf ist) l)
+    IntroInjection (List.map (intern_intro_pattern lf ist) l)
   | IntroWildcard | IntroRewrite _ as x -> x
-  | IntroApplyOn ((loc,c),pat) ->
-      IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat)
+  | IntroApplyOn ({loc;v=c},pat) ->
+    IntroApplyOn (make ?loc @@ intern_constr ist c, intern_intro_pattern lf ist pat)
 
 and intern_or_and_intro_pattern lf ist = function
    | IntroAndPattern l ->
@@ -256,10 +256,10 @@ let intern_or_and_intro_pattern_loc lf ist = function
   | ArgVar {v=id} as x ->
       if find_var id ist then x
       else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
-  | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
+  | ArgArg ll -> ArgArg (map (fun l -> intern_or_and_intro_pattern lf ist l) ll)
 
-let intern_intro_pattern_naming_loc lf ist (loc,pat) =
-  (loc,intern_intro_pattern_naming lf ist pat)
+let intern_intro_pattern_naming_loc lf ist = map (fun pat ->
+    intern_intro_pattern_naming lf ist pat)
 
   (* TODO: catch ltac vars *)
 let intern_destruction_arg ist = function
@@ -268,15 +268,15 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent {loc;v=id} ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
+        let c, p = intern_constr ist (make @@ CRef (Ident (Loc.tag id), None)) in
 	match DAst.get c with
-        | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id)
+        | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id)
 	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
       else
-        clear,ElimOnIdent CAst.(make ?loc id)
+        clear,ElimOnIdent (make ?loc id)
 
 let short_name = function
-  | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id)
+  | AN (Ident (loc,id)) when not !strict_check -> Some (make ?loc id)
   | _ -> None
 
 let intern_evaluable_global_reference ist r =
@@ -289,16 +289,16 @@ let intern_evaluable_global_reference ist r =
 
 let intern_evaluable_reference_or_by_notation ist = function
   | AN r -> intern_evaluable_global_reference ist r
-  | ByNotation (loc,(ntn,sc)) ->
+  | ByNotation {loc;v=(ntn,sc)} ->
       evaluable_of_global_reference ist.genv
       (Notation.interp_notation_as_global_reference ?loc
         (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
 (* Globalize a reduction expression *)
 let intern_evaluable ist = function
-  | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id)
+  | AN (Ident (loc,id)) when find_var id ist -> ArgVar (make ?loc id)
   | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist ->
-      ArgArg (EvalVarRef id, Some CAst.(make ?loc id))
+      ArgArg (EvalVarRef id, Some (make ?loc id))
   | r ->
       let e = intern_evaluable_reference_or_by_notation ist r in
       let na = short_name r in
@@ -817,7 +817,7 @@ let notation_subst bindings tac =
   let fold id c accu =
     let loc = Glob_ops.loc_of_glob_constr (fst c) in
     let c = ConstrMayEval (ConstrTerm c) in
-    (CAst.make ?loc @@ Name id, c) :: accu
+    (make ?loc @@ Name id, c) :: accu
   in
   let bindings = Id.Map.fold fold bindings [] in
   (** This is theoretically not correct due to potential variable capture, but
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 991afe9c6..a287b13b9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -247,7 +247,7 @@ let coerce_to_tactic loc id v =
     | _ -> fail ()
   else fail ()
 
-let intro_pattern_of_ident id = (Loc.tag @@ IntroNaming (IntroIdentifier id))
+let intro_pattern_of_ident id = make @@ IntroNaming (IntroIdentifier id)
 let value_of_ident id =
   in_gen (topwit wit_intro_pattern) (intro_pattern_of_ident id)
 
@@ -423,7 +423,7 @@ let extract_ltac_constr_values ist env =
     could barely be defined as a feature... *)
 
 (* Extract the identifier list from lfun: join all branches (what to do else?)*)
-let rec intropattern_ids accu (loc,pat) = match pat with
+let rec intropattern_ids accu {loc;v=pat} = match pat with
   | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu
   | IntroAction (IntroOrAndPattern (IntroAndPattern l)) ->
       List.fold_left intropattern_ids accu l
@@ -431,7 +431,7 @@ let rec intropattern_ids accu (loc,pat) = match pat with
       List.fold_left intropattern_ids accu (List.flatten ll)
   | IntroAction (IntroInjection l) ->
       List.fold_left intropattern_ids accu l
-  | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat
+  | IntroAction (IntroApplyOn ({v=c},pat)) -> intropattern_ids accu pat
   | IntroNaming (IntroAnonymous | IntroFresh _)
   | IntroAction (IntroWildcard | IntroRewrite _)
   | IntroForthcoming _ -> accu
@@ -439,9 +439,9 @@ let rec intropattern_ids accu (loc,pat) = match pat with
 let extract_ids ids lfun accu =
   let fold id v accu =
     if has_type v (topwit wit_intro_pattern) then
-      let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
+      let {v=ipat} = out_gen (topwit wit_intro_pattern) v in
       if Id.List.mem id ids then accu
-      else intropattern_ids accu (Loc.tag ipat)
+      else intropattern_ids accu (make ipat)
     else accu
   in
   Id.Map.fold fold lfun accu
@@ -762,15 +762,15 @@ let interp_message ist l =
   Ftactic.List.map (interp_message_token ist) l >>= fun l ->
   Ftactic.return (prlist_with_sep spc (fun x -> x) l)
 
-let rec interp_intro_pattern ist env sigma = function
-  | loc, IntroAction pat ->
-      let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
-      sigma, (loc, IntroAction pat)
-  | loc, IntroNaming (IntroIdentifier id) ->
-      sigma, (loc, interp_intro_pattern_var loc ist env sigma id)
-  | loc, IntroNaming pat ->
-      sigma, (loc, IntroNaming (interp_intro_pattern_naming loc ist env sigma pat))
-  | loc, IntroForthcoming _  as x -> sigma, x
+let rec interp_intro_pattern ist env sigma = with_loc_val (fun ?loc -> function
+  | IntroAction pat ->
+    let (sigma,pat) = interp_intro_pattern_action ist env sigma pat in
+    sigma, make ?loc @@ IntroAction pat
+  | IntroNaming (IntroIdentifier id) ->
+    sigma, make ?loc @@ interp_intro_pattern_var loc ist env sigma id
+  | IntroNaming pat ->
+    sigma, make ?loc @@ IntroNaming (interp_intro_pattern_naming loc ist env sigma pat)
+  | IntroForthcoming _  as x -> sigma, make ?loc x)
 
 and interp_intro_pattern_naming loc ist env sigma = function
   | IntroFresh id -> IntroFresh (interp_ident ist env sigma id)
@@ -784,10 +784,10 @@ and interp_intro_pattern_action ist env sigma = function
   | IntroInjection l ->
       let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
       sigma, IntroInjection l
-  | IntroApplyOn ((loc,c),ipat) ->
+  | IntroApplyOn ({loc;v=c},ipat) ->
       let c env sigma = interp_open_constr ist env sigma c in
       let sigma,ipat = interp_intro_pattern ist env sigma ipat in
-      sigma, IntroApplyOn ((loc,c),ipat)
+      sigma, IntroApplyOn (make ?loc c,ipat)
   | IntroWildcard | IntroRewrite _ as x -> sigma, x
 
 and interp_or_and_intro_pattern ist env sigma = function
@@ -799,7 +799,7 @@ and interp_or_and_intro_pattern ist env sigma = function
       sigma, IntroOrPattern ll
 
 and interp_intro_pattern_list_as_list ist env sigma = function
-  | [loc,IntroNaming (IntroIdentifier id)] as l ->
+  | [{loc;v=IntroNaming (IntroIdentifier id)}] as l ->
       (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ ->
          List.fold_left_map (interp_intro_pattern ist env) sigma l)
@@ -807,18 +807,18 @@ and interp_intro_pattern_list_as_list ist env sigma = function
 
 let interp_intro_pattern_naming_option ist env sigma = function
   | None -> None
-  | Some (loc,pat) -> Some (loc, interp_intro_pattern_naming loc ist env sigma pat)
+  | Some lpat -> Some (map_with_loc (fun ?loc pat -> interp_intro_pattern_naming loc ist env sigma pat) lpat)
 
 let interp_or_and_intro_pattern_option ist env sigma = function
   | None -> sigma, None
   | Some (ArgVar {loc;v=id}) ->
       (match interp_intro_pattern_var loc ist env sigma id with
-      | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
+      | IntroAction (IntroOrAndPattern l) -> sigma, Some (make ?loc l)
       | _ ->
         user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern."))
-  | Some (ArgArg (loc,l)) ->
+  | Some (ArgArg {loc;v=l}) ->
       let sigma,l = interp_or_and_intro_pattern ist env sigma l in
-      sigma, Some (loc,l)
+      sigma, Some (make ?loc l)
 
 let interp_intro_pattern_option ist env sigma = function
   | None -> sigma, None
@@ -846,9 +846,9 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
             (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
-let interp_binding ist env sigma (loc,(b,c)) =
+let interp_binding ist env sigma {loc;v=(b,c)} =
   let sigma, c = interp_open_constr ist env sigma c in
-  sigma, (loc,(interp_binding_name ist env sigma b,c))
+  sigma, (make ?loc (interp_binding_name ist env sigma b,c))
 
 let interp_bindings ist env sigma = function
 | NoBindings ->
@@ -873,7 +873,7 @@ let interp_open_constr_with_bindings ist env sigma (c,bl) =
 let loc_of_bindings = function
 | NoBindings         -> None
 | ImplicitBindings l -> loc_of_glob_constr (fst (List.last l))
-| ExplicitBindings l -> fst (List.last l)
+| ExplicitBindings l -> (List.last l).loc
 
 let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) =
   let loc1 = loc_of_glob_constr c in
@@ -896,7 +896,7 @@ let interp_destruction_arg ist gl arg =
       in
       let try_cast_id id' =
         if Tactics.is_quantified_hypothesis id' gl
-        then keep,ElimOnIdent CAst.(make ?loc id')
+        then keep,ElimOnIdent (make ?loc id')
         else
           (keep, ElimOnConstr begin fun env sigma ->
           try (sigma, (constr_of_id env id', NoBindings))
@@ -911,7 +911,7 @@ let interp_destruction_arg ist gl arg =
         if has_type v (topwit wit_intro_pattern) then
           let v = out_gen (topwit wit_intro_pattern) v in
           match v with
-          | _, IntroNaming (IntroIdentifier id) -> try_cast_id id
+          | {v=IntroNaming (IntroIdentifier id)} -> try_cast_id id
           | _ -> error ()
         else if has_type v (topwit wit_var) then
           let id = out_gen (topwit wit_var) v in
@@ -924,9 +924,9 @@ let interp_destruction_arg ist gl arg =
       with Not_found ->
 	(* We were in non strict (interactive) mode *)
 	if Tactics.is_quantified_hypothesis id gl then
-          keep,ElimOnIdent CAst.(make ?loc id)
+          keep,ElimOnIdent (make ?loc id)
 	else
-          let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+          let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (Ident (loc,id),None))) in
           let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
             (sigma, (c,NoBindings))
@@ -1221,7 +1221,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
   | TacFreshId l ->
       Ftactic.enter begin fun gl ->
         let id = interp_fresh_id ist (pf_env gl) (project gl) l in
-        Ftactic.return (in_gen (topwit wit_intro_pattern) (Loc.tag @@ IntroNaming (IntroIdentifier id)))
+        Ftactic.return (in_gen (topwit wit_intro_pattern) (make @@ IntroNaming (IntroIdentifier id)))
       end
   | TacPretype c ->
       Ftactic.enter begin fun gl ->
@@ -1576,7 +1576,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = project gl in
 	let l = List.map (fun (k,c) ->
           let loc, f = interp_open_constr_with_bindings_loc ist c in
-	    (k,(loc,f))) cb 
+            (k,(make ?loc f))) cb
 	in
         let sigma,tac = match cl with
           | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
@@ -1677,7 +1677,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
           let flags = open_constr_use_classes_flags () in
           let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
           let let_tac b na c cl eqpat =
-            let id = Option.default (Loc.tag IntroAnonymous) eqpat in
+            let id = Option.default (make IntroAnonymous) eqpat in
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
@@ -1689,7 +1689,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
-            let id = Option.default (Loc.tag IntroAnonymous) eqpat in
+            let id = Option.default (make IntroAnonymous) eqpat in
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_pat_tac ev with_eq na c cl
           in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 927139c1a..a1d8b087e 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -33,8 +33,9 @@ let subst_glob_constr_and_expr subst (c, e) =
 
 let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
 
-let subst_binding subst (loc,(b,c)) =
-  (loc,(subst_quantified_hypothesis subst b,subst_glob_constr subst c))
+let subst_binding subst =
+  CAst.map (fun (b,c) ->
+      subst_quantified_hypothesis subst b,subst_glob_constr subst c)
 
 let subst_bindings subst = function
   | NoBindings -> NoBindings
@@ -47,13 +48,13 @@ let subst_glob_with_bindings subst (c,bl) =
 let subst_glob_with_bindings_arg subst (clear,c) =
   (clear,subst_glob_with_bindings subst c)
 
-let rec subst_intro_pattern subst = function
-  | loc,IntroAction p -> loc, IntroAction (subst_intro_pattern_action subst p)
-  | loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
+let rec subst_intro_pattern subst = CAst.map (function
+  | IntroAction p -> IntroAction (subst_intro_pattern_action subst p)
+  | IntroNaming _ | IntroForthcoming _ as x -> x)
 
-and subst_intro_pattern_action subst = function
-  | IntroApplyOn ((loc,t),pat) ->
-      IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat)
+and subst_intro_pattern_action subst = let open CAst in function
+  | IntroApplyOn ({loc;v=t},pat) ->
+    IntroApplyOn (make ?loc @@ subst_glob_constr subst t,subst_intro_pattern subst pat)
   | IntroOrAndPattern l ->
       IntroOrAndPattern (subst_intro_or_and_pattern subst l)
   | IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)