Fixing bug #2640 and variants of it (inconsistency between when and

how the names of an ltac expression are globalized - allowing the
expression to be a constr and in some initial context - and when and
how this ltac expression is interpreted - now expecting a pure tactic
in a different context).

This incidentally found a Ltac bug in Ncring_polynom!

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

4 files changed, 22 insertions, 22 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index e71d53bf9..2f129637d 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -20,7 +20,7 @@ open Tok
 let fail_default_value = ArgArg 0
 
 let arg_of_expr = function
-    TacArg a -> a
+    TacArg (loc,a) -> a
   | e -> Tacexp (e:raw_tactic_expr)
 
 (* Tactics grammar rules *)
@@ -85,20 +85,20 @@ GEXTEND Gram
       | IDENT "fail"; n = [ n = int_or_var -> n | -> fail_default_value ];
 	  l = LIST0 message_token -> TacFail (n,l)
       | IDENT "external"; com = STRING; req = STRING; la = LIST1 tactic_arg ->
-	  TacArg (TacExternal (loc,com,req,la))
+	  TacArg (loc,TacExternal (loc,com,req,la))
       | st = simple_tactic -> TacAtom (loc,st)
-      | a = may_eval_arg -> TacArg(a)
+      | a = may_eval_arg -> TacArg(loc,a)
       | IDENT "constr"; ":"; id = METAIDENT ->
-          TacArg(MetaIdArg (loc,false,id))
+          TacArg(loc,MetaIdArg (loc,false,id))
       | IDENT "constr"; ":"; c = Constr.constr ->
-          TacArg(ConstrMayEval(ConstrTerm c))
+          TacArg(loc,ConstrMayEval(ConstrTerm c))
       | IDENT "ipattern"; ":"; ipat = simple_intropattern ->
-	  TacArg(IntroPattern ipat)
+	  TacArg(loc,IntroPattern ipat)
       | r = reference; la = LIST0 tactic_arg ->
-          TacArg(TacCall (loc,r,la)) ]
+          TacArg(loc,TacCall (loc,r,la)) ]
     | "0"
       [ "("; a = tactic_expr; ")" -> a
-      | a = tactic_atom -> TacArg a ] ]
+      | a = tactic_atom -> TacArg (loc,a) ] ]
   ;
   (* binder_tactic: level 5 of tactic_expr *)
   binder_tactic:
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fd4c1bcea..f55ced809 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -479,7 +479,7 @@ let pr_funvar = function
 
 let pr_let_clause k pr (id,(bl,t)) =
   hov 0 (str k ++ pr_lident id ++ prlist pr_funvar bl ++
-         str " :=" ++ brk (1,1) ++ pr (TacArg t))
+         str " :=" ++ brk (1,1) ++ pr (TacArg (dummy_loc,t)))
 
 let pr_let_clauses recflag pr = function
   | hd::tl ->
@@ -922,20 +922,20 @@ let rec pr_tac inherited tac =
       latom
   | TacAtom (loc,t) ->
       pr_with_comments loc (hov 1 (pr_atom1 t)), ltatom
-  | TacArg(Tacexp e) -> pr_tac_level (latom,E) e, latom
-  | TacArg(ConstrMayEval (ConstrTerm c)) ->
+  | TacArg(_,Tacexp e) -> pr_tac_level (latom,E) e, latom
+  | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
       str "constr:" ++ pr_constr c, latom
-  | TacArg(ConstrMayEval c) ->
+  | TacArg(_,ConstrMayEval c) ->
       pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c, leval
-  | TacArg(TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
-  | TacArg(Integer n) -> int n, latom
-  | TacArg(TacCall(loc,f,[])) -> pr_ref f, latom
-  | TacArg(TacCall(loc,f,l)) ->
+  | TacArg(_,TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom
+  | TacArg(_,Integer n) -> int n, latom
+  | TacArg(_,TacCall(loc,f,[])) -> pr_ref f, latom
+  | TacArg(_,TacCall(loc,f,l)) ->
       pr_with_comments loc
         (hov 1 (pr_ref f ++ spc () ++
          prlist_with_sep spc pr_tacarg l)),
       lcall
-  | TacArg a -> pr_tacarg a, latom
+  | TacArg (_,a) -> pr_tacarg a, latom
   in
   if prec_less prec inherited then strm
   else str"(" ++ strm ++ str")"
@@ -954,7 +954,7 @@ and pr_tacarg = function
       str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++
       spc() ++ prlist_with_sep spc pr_tacarg la
   | (TacCall _|Tacexp _|Integer _) as a ->
-      str "ltac:" ++ pr_tac (latom,E) (TacArg a)
+      str "ltac:" ++ pr_tac (latom,E) (TacArg (dummy_loc,a))
 
 in (pr_tac, pr_match_rule)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e184eafe3..7df97a075 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -465,9 +465,9 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
       <:expr< Tacexpr.TacFun
         ($mlexpr_of_list mlexpr_of_ident_option idol$,
          $mlexpr_of_tactic body$) >>
-  | Tacexpr.TacArg (Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
-  | Tacexpr.TacArg t ->
-      <:expr< Tacexpr.TacArg $mlexpr_of_tactic_arg t$ >>
+  | Tacexpr.TacArg (_,Tacexpr.MetaIdArg (_,true,id)) -> anti loc id
+  | Tacexpr.TacArg (_,t) ->
+      <:expr< Tacexpr.TacArg $dloc$ $mlexpr_of_tactic_arg t$ >>
   | Tacexpr.TacComplete t ->
       <:expr< Tacexpr.TacComplete $mlexpr_of_tactic t$ >>
   | _ -> failwith "Quotation of tactic expressions: TODO"
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 747d2c738..83dae3dce 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -16,7 +16,7 @@ open Logic
 open Printer
 
 let pr_tactic = function
-  | TacArg (Tacexp t) ->
+  | TacArg (_,Tacexp t) ->
       (*top tactic from tacinterp*)
       Pptactic.pr_glob_tactic (Global.env()) t
   | t ->