[location] Use located in tactics.

One case missing due the TACTIC EXTEND macro.

11 files changed, 38 insertions, 41 deletions

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index dffd90be3..d6cbd8db1 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -161,7 +161,7 @@ GEXTEND Gram
       | st = simple_tactic -> st
       | a = tactic_arg -> TacArg(!@loc,a)
       | r = reference; la = LIST0 tactic_arg_compat ->
-          TacArg(!@loc,TacCall (!@loc,r,la)) ]
+          TacArg(!@loc, TacCall (!@loc,(r,la))) ]
     | "0"
       [ "("; a = tactic_expr; ")" -> a
       | "["; ">"; (tf,tail) = tactic_then_gen; "]" ->
@@ -219,7 +219,7 @@ GEXTEND Gram
   ;
   tactic_atom:
     [ [ n = integer -> TacGeneric (genarg_of_int n)
-      | r = reference -> TacCall (!@loc,r,[])
+      | r = reference -> TacCall (!@loc,(r,[]))
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
   match_key:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 0dd6819fd..ae596c411 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1048,9 +1048,9 @@ type 'a extra_genarg_printer =
               primitive "fresh" ++ pr_fresh_ids l, latom
             | TacArg(_,TacGeneric arg) ->
               pr.pr_generic arg, latom
-            | TacArg(_,TacCall(loc,f,[])) ->
+            | TacArg(_,TacCall(loc,(f,[]))) ->
               pr.pr_reference f, latom
-            | TacArg(_,TacCall(loc,f,l)) ->
+            | TacArg(_,TacCall(loc,(f,l))) ->
               pr_with_comments loc (hov 1 (
                 pr.pr_reference f ++ spc ()
                 ++ prlist_with_sep spc pr_tacarg l)),
@@ -1059,7 +1059,7 @@ type 'a extra_genarg_printer =
               pr_tacarg a, latom
             | TacML (loc,s,l) ->
               pr_with_comments loc (pr.pr_extend 1 s l), lcall
-            | TacAlias (loc,kn,l) ->
+            | TacAlias (loc,(kn,l)) ->
               pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
           )
           in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1f75f88d4..40484bfea 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1969,7 +1969,7 @@ let make_tactic name =
   let loc = Loc.ghost in
   let tacpath = Libnames.qualid_of_string name in
   let tacname = Qualid (loc, tacpath) in
-  TacArg (loc, TacCall (loc, tacname, []))
+  TacArg (loc, TacCall (Loc.tag ~loc (tacname, [])))
 
 let add_morphism_infer glob m n =
   init_setoid ();
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cd8c9e471..39121ac94 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state =
         TacGeneric arg
     in
     let l = List.map map l in
-    (TacAlias (loc,kn,l):raw_tactic_expr)
+    (TacAlias (loc,(kn,l)):raw_tactic_expr)
   in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 8aefe7605..e8e99fcfe 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -184,8 +184,7 @@ type 'a gen_tactic_arg =
   | TacGeneric     of 'lev generic_argument
   | ConstrMayEval  of ('trm,'cst,'pat) may_eval
   | Reference      of 'ref
-  | TacCall of Loc.t * 'ref *
-      'a gen_tactic_arg list
+  | TacCall    of ('ref * 'a gen_tactic_arg list) Loc.located
   | TacFreshId of string or_var list
   | Tacexp of 'tacexpr
   | TacPretype of 'trm
@@ -207,7 +206,7 @@ constraint 'a = <
     'r : ltac refs, 'n : idents, 'l : levels *)
 
 and 'a gen_tactic_expr =
-  | TacAtom of Loc.t * 'a gen_atomic_tactic_expr
+  | TacAtom of ('a gen_atomic_tactic_expr) Loc.located
   | TacThen of
       'a gen_tactic_expr *
       'a gen_tactic_expr
@@ -268,7 +267,7 @@ and 'a gen_tactic_expr =
   (* For ML extensions *)
   | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list
   (* For syntax extensions *)
-  | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list
+  | TacAlias of (KerName.t * 'a gen_tactic_arg list) Loc.located
 
 constraint 'a = <
     term:'t;
@@ -389,7 +388,7 @@ type ltac_call_kind =
   | LtacVarCall of Id.t * glob_tactic_expr
   | LtacConstrInterp of Glob_term.glob_constr * Pretyping.ltac_var_map
 
-type ltac_trace = (Loc.t * ltac_call_kind) list
+type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
   | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ad9814b84..df845b1a4 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -126,7 +126,7 @@ let intern_move_location ist = function
 
 let intern_isolated_global_tactic_reference r =
   let (loc,qid) = qualid_of_reference r in
-  TacCall (loc,ArgArg (loc,locate_tactic qid),[])
+  TacCall (Loc.tag ~loc (ArgArg (loc,locate_tactic qid),[]))
 
 let intern_isolated_tactic_reference strict ist r =
   (* An ltac reference *)
@@ -624,12 +624,12 @@ and intern_tactic_seq onlytac ist = function
       ist.ltacvars, TacSelect (sel, intern_pure_tactic ist tac)
 
   (* For extensions *)
-  | TacAlias (loc,s,l) ->
+  | TacAlias (loc,(s,l)) ->
       let l = List.map (intern_tacarg !strict_check false ist) l in
-      ist.ltacvars, TacAlias (loc,s,l)
+      ist.ltacvars, TacAlias (Loc.tag ~loc (s,l))
   | TacML (loc,opn,l) ->
       let _ignore = Tacenv.interp_ml_tactic opn in
-      ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l)
+      ist.ltacvars, TacML (adjust_loc 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
@@ -650,11 +650,11 @@ 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,
+  | TacCall (loc,(f,[])) -> intern_isolated_tactic_reference strict ist f
+  | TacCall (loc,(f,l)) ->
+      TacCall (Loc.tag ~loc (
         intern_applied_tactic_reference ist f,
-        List.map (intern_tacarg !strict_check false ist) l)
+        List.map (intern_tacarg !strict_check false ist) l))
   | TacFreshId x -> TacFreshId (List.map (intern_string_or_var ist) x)
   | TacPretype c -> TacPretype (intern_constr ist c)
   | TacNumgoals -> TacNumgoals
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index aac63fcb2..64eda28ed 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1257,7 +1257,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,(s,l)) ->
       let (ids, body) = Tacenv.interp_alias s in
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
@@ -1341,9 +1341,9 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
         let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
         Sigma.Unsafe.of_pair (Ftactic.return (Value.of_constr c_interp), sigma)
       end }
-  | TacCall (loc,r,[]) ->
+  | TacCall (loc,(r,[])) ->
       interp_ltac_reference loc true ist r
-  | TacCall (loc,f,l) ->
+  | TacCall (loc,(f,l)) ->
       let (>>=) = Ftactic.bind in
       interp_ltac_reference loc true ist f >>= fun fv ->
       Ftactic.List.map (fun a -> interp_tacarg ist a) l >>= fun largs ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 9582ebd89..c92dd23a0 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -77,9 +77,7 @@ let subst_or_var f =  function
   | ArgVar _ as x -> x
   | ArgArg x -> ArgArg (f x)
 
-let dloc = Loc.ghost
-
-let subst_located f (_loc,id) = (dloc,f id)
+let subst_located f = Loc.map f
 
 let subst_reference subst =
   subst_or_var (subst_located (subst_kn subst))
@@ -182,7 +180,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 (dloc, subst_atomic subst t)
+  | TacAtom (_loc,t) -> TacAtom (Loc.tag @@ 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
@@ -229,22 +227,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 (dloc,subst_tacarg subst a)
+  | TacArg (_,a) -> TacArg (Loc.tag @@ subst_tacarg subst a)
   | TacSelect (s, tac) -> TacSelect (s, subst_tactic subst tac)
 
   (* For extensions *)
-  | TacAlias (_,s,l) ->
+  | TacAlias (_,(s,l)) ->
       let s = subst_kn subst s in
-      TacAlias (dloc,s,List.map (subst_tacarg subst) l)
-  | TacML (_loc,opn,l) -> TacML (dloc,opn,List.map (subst_tacarg subst) l)
+      TacAlias (Loc.tag (s,List.map (subst_tacarg subst) l))
+  | TacML (_loc,opn,l) -> TacML (_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, subst_reference subst f, List.map (subst_tacarg subst) l)
+  | TacCall (loc,(f,l)) ->
+      TacCall (Loc.tag ~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/tauto.ml b/plugins/ltac/tauto.ml
index dc7ee6a23..30eed08d7 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -264,7 +264,7 @@ let with_flags flags _ ist =
   let x = (loc, Id.of_string "x") in
   let arg = Val.Dyn (tag_tauto_flags, flags) in
   let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in
-  eval_tactic_ist ist (TacArg (loc, TacCall (loc, ArgVar f, [Reference (ArgVar x)])))
+  eval_tactic_ist ist (TacArg (loc, TacCall (loc, (ArgVar f, [Reference (ArgVar x)]))))
 
 let register_tauto_tactic tac name0 args =
   let ids = List.map (fun id -> Id.of_string id) args in
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 6c3e66112..432625e4d 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -25,7 +25,7 @@ let x = Id.of_string "x"
 
 let make_cont (k : Val.t) (c : EConstr.t) =
   let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (loc, ArgVar (loc, cont), [Reference (ArgVar (loc, x))]) in
+  let tac = TacCall (loc, (ArgVar (loc, cont), [Reference (ArgVar (loc, x))])) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
   Tacinterp.eval_tactic_ist ist (TacArg (loc, tac))
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index bef8139be..e3e14bcf3 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -161,11 +161,11 @@ let decl_constant na ctx c =
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgArg(Loc.ghost, Lazy.force tac),args))
+  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgArg(Loc.tag @@ Lazy.force tac),args)))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
+  TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args)))
 
 let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
   let fold arg (i, vars, lfun) =
@@ -580,8 +580,8 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
     | Some (Closed lc) ->
         closed_term_ast (List.map Smartlocate.global_with_alias lc)
     | None ->
-        let t = ArgArg(Loc.ghost,Lazy.force ltac_inv_morph_nothing) in
-              TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
+        let t = ArgArg(Loc.tag @@ Lazy.force ltac_inv_morph_nothing) in
+              TacArg(Loc.tag (TacCall(Loc.tag (t,[]))))
 
 let make_hyp env evd c =
   let t = Retyping.get_type_of env !evd c in
@@ -602,8 +602,8 @@ let interp_power env evd pow =
   let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
   match pow with
   | None ->
-      let t = ArgArg(Loc.ghost, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(Loc.ghost,TacCall(Loc.ghost,t,[])), plapp evd coq_None [|carrier|])
+      let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
+      (TacArg(Loc.ghost,TacCall(Loc.tag (t,[]))), plapp evd coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with