Localisation des appels de tactiques définies sans arguments

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3922 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 12 insertions, 12 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3c894dd84..1147e84fd 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -671,7 +671,7 @@ let rec glob_printers =
      Printer.pr_pattern,
      pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)),
      pr_or_var pr_inductive,
-     pr_or_var pr_ltac_constant,
+     pr_or_var (pr_located pr_ltac_constant),
      pr_located pr_id,
      pr_glob_extend)
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a2584773f..0fd4130d2 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -245,7 +245,7 @@ type glob_tactic_expr =
      constr_pattern,
      evaluable_global_reference and_short_name or_var or_metanum,
      inductive or_var or_metanum,
-     ltac_constant or_var,
+     ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_tactic_expr
 
@@ -254,7 +254,7 @@ type glob_atomic_tactic_expr =
      constr_pattern,
      evaluable_global_reference and_short_name or_var or_metanum,
      inductive or_var or_metanum,
-     ltac_constant or_var,
+     ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_atomic_tactic_expr
 
@@ -263,7 +263,7 @@ type glob_tactic_arg =
      constr_pattern,
      evaluable_global_reference and_short_name or_var or_metanum,
      inductive or_var or_metanum,
-     ltac_constant or_var,
+     ltac_constant located or_var,
      identifier located,
      glob_tactic_expr) gen_tactic_arg
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 514557d34..a58220238 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -369,12 +369,12 @@ let intern_global_reference ist = function
 let intern_tac_ref ist = function
   | Ident (loc,id) when find_ltacvar id ist -> ArgVar (loc,id)
   | Ident (loc,id) ->
-      ArgArg
-        (try find_recvar id ist 
+      ArgArg (loc,
+         try find_recvar id ist 
          with Not_found -> locate_tactic (make_short_qualid id))
   | r -> 
       let (loc,qid) = qualid_of_reference r in
-      ArgArg (locate_tactic qid)
+      ArgArg (loc,locate_tactic qid)
 
 let intern_tactic_reference ist r =
   try intern_tac_ref ist r
@@ -726,8 +726,8 @@ and intern_tacarg strict ist = function
       let id = id_of_string s in
       if find_ltacvar id ist then Reference (ArgVar (dummy_loc,strip_meta id))
       else error_syntactic_metavariables_not_allowed loc
-  | TacCall (_loc,f,l) ->
-      TacCall (_loc,
+  | TacCall (loc,f,l) ->
+      TacCall (loc,
         intern_tactic_reference ist f,
         List.map (intern_tacarg !strict_check ist) l)
   | Tacexp t -> Tacexp (intern_tactic ist t)
@@ -1280,8 +1280,8 @@ and eval_tactic ist = function
 
 and interp_ltac_reference isapplied ist gl = function
   | ArgVar (loc,id) -> unrec (List.assoc id ist.lfun)
-  | ArgArg qid ->
-      let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup qid) in
+  | ArgArg (loc,r) ->
+      let v = val_interp {lfun=[];lmatch=[];debug=ist.debug} gl (lookup r) in
       if isapplied then v else locate_tactic_call loc v
 
 and interp_tacarg ist gl = function
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 157999b10..0cc3234c2 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -519,7 +519,7 @@ let rec glob_printers =
      Printer.pr_pattern,
      pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)),
      (fun vars -> pr_or_var (pr_inductive vars)),
-     pr_or_var pr_ltac_constant,
+     pr_or_var (pr_located pr_ltac_constant),
      pr_located pr_id,
      Pptactic.pr_glob_extend)