Hack pour autoriser les $n dans les Grammar tactic

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

1 files changed, 8 insertions, 4 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 99ed8aeb1..0a219ddc9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1140,16 +1140,20 @@ and tacarg_interp ist = function
   | Integer n -> VInteger n
   | ConstrMayEval c -> VConstr (constr_interp_may_eval ist c)
   | MetaNumArg (_,n) -> VConstr (List.assoc n ist.lmatch)
-  | MetaIdArg (loc,_) -> error_syntactic_metavariables_not_allowed loc
-(*
-  | Tacexp t -> VArg (Tacexp ((*tactic_interp ist t,*)t))
-*)
+  | MetaIdArg (loc,id) ->
+      (try (* $id can occur in Grammar tactic... *)
+        (unrec (List.assoc (id_of_string id) ist.lfun))
+      with
+        | Not_found -> error_syntactic_metavariables_not_allowed loc)
   | TacCall (loc,f,l) ->
       let fv = tacarg_interp ist f
       and largs = List.map (tacarg_interp ist) l in
       app_interp ist fv largs loc
   | Tacexp t -> val_interp ist t
 (*
+  | Tacexp t -> VArg (Tacexp ((*tactic_interp ist t,*)t))
+*)
+(*
     | Node(loc,s,l) ->
         let fv = val_interp ist (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
         and largs = List.map (val_interp ist) l in