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

6 files changed, 15 insertions, 15 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 64aa08ff2..b3e076c49 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -27,7 +27,7 @@ let intern_justification_items globs =
   Option.map (List.map (intern_constr globs))
 
 let intern_justification_method globs =
-  Option.map (intern_tactic globs)
+  Option.map (intern_pure_tactic globs)
 
 let intern_statement intern_it globs st =
   {st_label=st.st_label;
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v
index a3e14b30f..c0d315871 100644
--- a/plugins/setoid_ring/Ncring_polynom.v
+++ b/plugins/setoid_ring/Ncring_polynom.v
@@ -23,7 +23,7 @@ Context (C R:Type) `{Rh:Ring_morphism C R}.
 
 Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x.
 
- Ltac rsimpl := repeat (gen_rewrite || phiCR_comm).
+ Ltac rsimpl := repeat (gen_rewrite || rewrite phiCR_comm).
  Ltac add_push := gen_add_push .
 
 (* Definition of non commutative multivariable polynomials 
@@ -298,7 +298,7 @@ reflexivity.
   induction P;simpl;intros.  rewrite ring_morphism_mul.
 try reflexivity.
   simpl. Esimpl.  rewrite IHP1;rewrite IHP2;rsimpl. 
-  repeat rewrite  phiCR_comm. Esimpl.  Qed.
+  Qed.
 
  Lemma PmulC_ok : forall c P l, (PmulC P c)@l ==  P@l * [c].
  Proof.
@@ -618,4 +618,4 @@ exact pow_th.
   apply Peq_ok;trivial.
  Qed.
 
-End MakeRingPol.
\ No newline at end of file
+End MakeRingPol.
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index af236bc0f..d189a4e55 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -164,11 +164,11 @@ let decl_constant na c =
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
+  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force tac),args))
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
+  TacArg(dummy_loc,TacCall(dummy_loc, ArgVar(dummy_loc, id_of_string tac),args))
 
 let ltac_letin (x, e1) e2 =
   TacLetIn(false,[(dummy_loc,id_of_string x),e1],e2)
@@ -624,23 +624,23 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
         (match rk, opp, kind with
             Abstract, None, _ ->
               let t = ArgArg(dummy_loc,Lazy.force ltac_inv_morphN) in
-              TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
+              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul]))
           | Abstract, Some opp, Some _ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphZ) in
-              TacArg(TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+              TacArg(dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | Abstract, Some opp, None ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morphNword) in
               TacArg
-                (TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
+                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;add;mul;opp]))
           | Computational _,_,_ ->
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
               TacArg
-                (TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
+                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;zero;one]))
           | Morphism mth,_,_ ->
               let (_,czero,cone,_,_,_,_,_,_) = dest_morph env sigma mth in
               let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_gen) in
               TacArg
-                (TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
+                (dummy_loc,TacCall(dummy_loc,t,List.map carg [zero;one;czero;cone])))
 
 let make_hyp env c =
   let t = Retyping.get_type_of env Evd.empty c in
@@ -657,7 +657,7 @@ let interp_power env pow =
   match pow with
   | None ->
       let t = ArgArg(dummy_loc, Lazy.force ltac_inv_morph_nothing) in
-      (TacArg(TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
+      (TacArg(dummy_loc,TacCall(dummy_loc,t,[])), lapp coq_None [|carrier|])
   | Some (tac, spec) ->
       let tac =
         match tac with
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index ae28c9847..546d720c4 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -474,4 +474,4 @@ let tactics_tac s =
   lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
 
 let tactics_call tac args =
-  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
+  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index 44a481f44..3c3e54fa3 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.ml4
@@ -42,7 +42,7 @@ let thin_sign osign sign =
 ;;
 
 let pr_tactic_xml = function
-  | TacArg (Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>"
+  | TacArg (_,Tacexp t) -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_glob_tactic (Global.env()) t) ++ str "\"/>"
   | t -> str "<tactic cmd=\"" ++ xmlstream (Pptactic.pr_tactic (Global.env()) t) ++ str "\"/>"
 ;;
 
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index b0e4fcc69..2f5eb6ac2 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -144,7 +144,7 @@ Pp.ppnl (Pp.(++) (Pp.str
          Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node
         in begin
         match tactic_expr with
-        | T.TacArg (T.Tacexp _) ->
+        | T.TacArg (_,T.Tacexp _) ->
             (* We don't need to keep the level of abstraction introduced at *)
             (* user-level invocation of tactic... (see Tacinterp.hide_interp)*)
             aux flat_proof old_hyps