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

14 files changed, 131 insertions, 94 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 ->
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
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 9e2acfdd0..b8279b8f9 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -240,7 +240,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
   | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
   | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast
-  | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg
+  | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_arg located
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_fun_ast =
   identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 90e4582fa..f9fba20e6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -60,6 +60,9 @@ let error_syntactic_metavariables_not_allowed loc =
     (loc,"out_ident",
      str "Syntactic metavariables allowed only in quotations.")
 
+let error_tactic_expected loc =
+  user_err_loc (loc,"",str "Tactic expected.")
+
 let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid
 
 let skip_metaid = function
@@ -189,7 +192,7 @@ let _ =
       (fun (s,t) -> add_primitive_tactic s t)
       [ "idtac",TacId [];
         "fail", TacFail(ArgArg 0,[]);
-        "fresh", TacArg(TacFreshId [])
+        "fresh", TacArg(dloc,TacFreshId [])
       ]
 
 let lookup_atomic id = Idmap.find id !atomic_mactab
@@ -696,7 +699,7 @@ let rec intern_atomic lf ist x =
       TacMutualCofix (b,intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
-      TacAssert (Option.map (intern_tactic ist) otac,
+      TacAssert (Option.map (intern_pure_tactic ist) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
                  intern_constr_gen false (otac<>None) ist c)
   | TacGeneralize cl ->
@@ -758,7 +761,7 @@ let rec intern_atomic lf ist x =
   | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
   | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
   | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll)
-  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t)
   | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
 
   (* Conversion *)
@@ -787,7 +790,7 @@ let rec intern_atomic lf ist x =
 	(ev,
 	List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
 	clause_app (intern_hyp_location ist) cl,
-	Option.map (intern_tactic ist) by)
+	Option.map (intern_pure_tactic ist) by)
   | TacInversion (inv,hyp) ->
       TacInversion (intern_inversion_strength lf ist inv,
         intern_quantified_hypothesis ist hyp)
@@ -800,9 +803,9 @@ let rec intern_atomic lf ist x =
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
       TacAlias (loc,s,l,(dir,body))
 
-and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr)
+and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
 
-and intern_tactic_seq ist = function
+and intern_tactic_seq onlytac ist = function
   | TacAtom (loc,t) ->
       let lf = ref ist.ltacvars in
       let t = intern_atomic lf ist t in
@@ -812,52 +815,68 @@ and intern_tactic_seq ist = function
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
       let l = List.map (fun (n,b) ->
-	  (n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in
-      ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u)
+	  (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
+      ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
+
   | TacMatchGoal (lz,lr,lmr) ->
-      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule ist lmr)
+      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)
   | TacMatch (lz,c,lmr) ->
-      ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
+      ist.ltacvars,
+      TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
   | TacId l -> ist.ltacvars, TacId (intern_message ist l)
   | TacFail (n,l) ->
       ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
-  | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
-  | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
+  | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
+  | TacAbstract (tac,s) ->
+      ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
   | TacThen (t1,[||],t2,[||]) ->
-      let lfun', t1 = intern_tactic_seq ist t1 in
-      let lfun'', t2 = intern_tactic_seq { ist with ltacvars = lfun' } t2 in
+      let lfun', t1 = intern_tactic_seq onlytac ist t1 in
+      let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in
       lfun'', TacThen (t1,[||],t2,[||])
   | TacThen (t1,tf,t2,tl) ->
-      let lfun', t1 = intern_tactic_seq ist t1 in
+      let lfun', t1 = intern_tactic_seq onlytac ist t1 in
       let ist' = { ist with ltacvars = lfun' } in
       (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun', TacThen (t1,Array.map (intern_tactic ist') tf,intern_tactic ist' t2,
-		       Array.map (intern_tactic ist') tl)
+      lfun', TacThen (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2,
+		       Array.map (intern_pure_tactic ist') tl)
   | TacThens (t,tl) ->
-      let lfun', t = intern_tactic_seq ist t in
+      let lfun', t = intern_tactic_seq true ist t in
       let ist' = { ist with ltacvars = lfun' } in
       (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun', TacThens (t, List.map (intern_tactic ist') tl)
+      lfun', TacThens (t, List.map (intern_pure_tactic ist') tl)
   | TacDo (n,tac) ->
-      ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
+      ist.ltacvars, TacDo (intern_or_var ist n,intern_pure_tactic ist tac)
+  | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac)
+  | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac)
+  | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
   | TacTimeout (n,tac) ->
-      ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic ist tac)
-  | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
-  | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
-  | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
+      ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac)
   | TacOrelse (tac1,tac2) ->
-      ist.ltacvars, TacOrelse (intern_tactic ist tac1,intern_tactic ist tac2)
-  | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_tactic ist) l)
-  | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_tactic ist) l)
-  | TacComplete tac -> ist.ltacvars, TacComplete (intern_tactic ist tac)
-  | TacArg a -> ist.ltacvars, TacArg (intern_tacarg true ist a)
+      ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
+  | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l)
+  | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
+  | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
+  | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+
+and intern_tactic_as_arg loc onlytac ist a =
+  match intern_tacarg !strict_check onlytac ist a with
+  | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a)
+  | Tacexp a -> a
+  | TacVoid | IntroPattern _ | Integer _
+  | ConstrMayEval _ | TacFreshId _ as a ->
+      if onlytac then error_tactic_expected loc else TacArg (loc,a)
+  | MetaIdArg _ -> assert false
+
+and intern_tactic_or_tacarg ist = intern_tactic false ist
+
+and intern_pure_tactic ist = intern_tactic true ist
 
 and intern_tactic_fun ist (var,body) =
   let (l1,l2) = ist.ltacvars in
   let lfun' = List.rev_append (Option.List.flatten var) l1 in
-  (var,intern_tactic { ist with ltacvars = (lfun',l2) } body)
+  (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body)
 
-and intern_tacarg strict ist = function
+and intern_tacarg strict onlytac ist = function
   | TacVoid -> TacVoid
   | Reference r -> intern_non_tactic_reference strict ist r
   | IntroPattern ipat ->
@@ -876,28 +895,29 @@ and intern_tacarg strict ist = function
   | TacCall (loc,f,l) ->
       TacCall (loc,
         intern_applied_tactic_reference ist f,
-        List.map (intern_tacarg !strict_check ist) l)
+        List.map (intern_tacarg !strict_check false ist) l)
   | TacExternal (loc,com,req,la) ->
-      TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la)
+      TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la)
   | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
-  | Tacexp t -> Tacexp (intern_tactic ist t)
+  | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
   | TacDynamic(loc,t) as x ->
       (match Dyn.tag t with
-	| "tactic" | "value" | "constr" -> x
+	| "tactic" | "value" -> x
+        | "constr" -> if onlytac then error_tactic_expected loc else x
 	| s -> anomaly_loc (loc, "",
                  str "Unknown dynamic: <" ++ str s ++ str ">"))
 
 (* Reads the rules of a Match Context or a Match *)
-and intern_match_rule ist = function
+and intern_match_rule onlytac ist = function
   | (All tc)::tl ->
-      All (intern_tactic ist tc) :: (intern_match_rule ist tl)
+      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
   | (Pat (rl,mp,tc))::tl ->
       let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
       let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
       let ido,metas2,pat = intern_pattern ist lfun mp in
       let metas = list_uniquize (metas1@metas2) in
       let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
-      Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl)
+      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
 
 and intern_genarg ist x =
@@ -953,7 +973,7 @@ and intern_genarg ist x =
       match tactic_genarg_level s with
       | Some n ->
           (* Special treatment of tactic arguments *)
-          in_gen (globwit_tactic n) (intern_tactic ist
+          in_gen (globwit_tactic n) (intern_tactic_or_tacarg ist
 	    (out_gen (rawwit_tactic n) x))
       | None ->
           lookup_genarg_glob s ist x
@@ -1727,7 +1747,7 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
   | TacLetIn (false,l,u) -> interp_letin ist gl l u
   | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr
   | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr
-  | TacArg a -> interp_tacarg ist gl a
+  | TacArg (loc,a) -> interp_tacarg ist gl a
   (* Delayed evaluation *)
   | t -> VFun (ist.trace,ist.lfun,[],t)
 
@@ -1768,7 +1788,7 @@ and eval_tactic ist = function
 	  begin
 	    match tac with
 		TacAtom (_,_) -> t
-	      | _ -> abstract_tactic_expr (TacArg (Tacexp tac)) t
+	      | _ -> abstract_tactic_expr (TacArg (dloc,Tacexp tac)) t
 	  end
   | TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
   | TacOrelse (tac1,tac2) ->
@@ -1892,7 +1912,7 @@ and eval_with_fail ist is_lazy goal tac =
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =
   let lref = ref ist.lfun in
-  let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg b))) llc in
+  let lve = list_map_left (fun ((_,id),b) -> (id,VRec (lref,TacArg (dloc,b)))) llc in
   lref := lve@ist.lfun;
   let ist = { ist with lfun = lve@ist.lfun } in
   val_interp ist gl u
@@ -2055,7 +2075,7 @@ and interp_genarg ist gl x =
       | Some n ->
           (* Special treatment of tactic arguments *)
           in_gen (wit_tactic n)
-	    (TacArg(valueIn(VFun(ist.trace,ist.lfun,[],
+	    (TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[],
 				 out_gen (globwit_tactic n) x))))
       | None ->
           lookup_interp_genarg s ist gl x
@@ -2463,7 +2483,7 @@ let make_empty_glob_sign () =
 (* Initial call for interpretation *)
 let interp_tac_gen lfun avoid_ids debug t gl =
   interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
-    (intern_tactic {
+    (intern_tactic true {
       ltacvars = (List.map fst lfun, []); ltacrecvars = [];
       gsigma = project gl; genv = pf_env gl } t) gl
 
@@ -2476,18 +2496,18 @@ let interp t = interp_tac_gen [] [] (get_debug()) t
 let eval_ltac_constr gl t =
   interp_ltac_constr
     { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl
-    (intern_tactic (make_empty_glob_sign ()) t )
+    (intern_tactic_or_tacarg (make_empty_glob_sign ()) t )
 
 (* Hides interpretation for pretty-print *)
 let hide_interp t ot gl =
   let ist = { ltacvars = ([],[]); ltacrecvars = [];
             gsigma = project gl; genv = pf_env gl } in
-  let te = intern_tactic ist t in
+  let te = intern_tactic true ist t in
   let t = eval_tactic te in
   match ot with
-  | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
+  | None -> abstract_tactic_expr (TacArg (dloc,Tacexp te)) t gl
   | Some t' ->
-      abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl
+      abstract_tactic_expr ~dflt:true (TacArg (dloc,Tacexp te)) (tclTHEN t t') gl
 
 (***************************************************************************)
 (* Substitution at module closing time *)
@@ -2715,7 +2735,7 @@ 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 (subst_tacarg subst a)
+  | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a)
 
 and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
 
@@ -2897,7 +2917,7 @@ let add_tacdef local isrec tacl =
   let gtacl =
     List.map2 (fun (_,b,def) (id, qid) ->
       let k = if b then UpdateTac qid else NewTac (Option.get id) in
-      let t = Flags.with_option strict_check (intern_tactic ist) def in
+      let t = Flags.with_option strict_check (intern_tactic_or_tacarg ist) def in
 	(k, t))
       tacl rfun in
   let id0 = fst (List.hd rfun) in
@@ -2915,11 +2935,11 @@ let add_tacdef local isrec tacl =
 (* Other entry points *)
 
 let glob_tactic x =
-  Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x
+  Flags.with_option strict_check (intern_tactic true (make_empty_glob_sign ())) x
 
 let glob_tactic_env l env x =
   Flags.with_option strict_check
-  (intern_tactic
+  (intern_pure_tactic
     { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
     x
 
@@ -2931,7 +2951,7 @@ let interp_redexp env sigma r =
 (***************************************************************************)
 (* Embed tactics in raw or glob tactic expr *)
 
-let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t))
+let globTacticIn t = TacArg (dloc,TacDynamic (dloc,tactic_in t))
 let tacticIn t =
   globTacticIn (fun ist ->
     try glob_tactic (t ist)
@@ -2940,7 +2960,7 @@ let tacticIn t =
        Errors.print e))
 
 let tacticOut = function
-  | TacArg (TacDynamic (_,d)) ->
+  | TacArg (_,TacDynamic (_,d)) ->
     if (Dyn.tag d) = "tactic" then
       tactic_out d
     else
@@ -2959,6 +2979,6 @@ let _ = Auto.set_extern_interp
 let _ = Auto.set_extern_intern_tac
   (fun l ->
     Flags.with_option strict_check
-    (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
+    (intern_pure_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
 let _ = Auto.set_extern_subst_tactic subst_tactic
 let _ = Dhyp.set_extern_interp eval_tactic
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 6d7909b3b..d9dc8094f 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -91,7 +91,7 @@ val interp_genarg :
 val intern_genarg :
   glob_sign -> raw_generic_argument -> glob_generic_argument
 
-val intern_tactic :
+val intern_pure_tactic :
   glob_sign -> raw_tactic_expr -> glob_tactic_expr
 
 val intern_constr :
diff --git a/test-suite/bugs/closed/shouldsucceed/2640.v b/test-suite/bugs/closed/shouldsucceed/2640.v
new file mode 100644
index 000000000..da0cc68a4
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2640.v
@@ -0,0 +1,17 @@
+(* Testing consistency of globalization and interpretation in some
+   extreme cases *)
+
+Section sect.
+
+  (* Simplification of the initial example *)
+  Hypothesis Other: True.
+
+  Lemma C2 : True.
+  proof.
+  Fail have True using Other.
+  Abort.
+
+  (* Variant of the same problem *)
+  Lemma C2 : True.
+  Fail clear; Other.
+  Abort.