From 80c2fb9228ece1d7ce2cc5e631ee24fa9bd7f843 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 3 Jul 2002 19:17:21 +0000
Subject: 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
---
 tactics/tacinterp.ml | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 99ed8aeb1a..0a219ddc9e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1140,15 +1140,19 @@ 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,[])]))
-- 
cgit v1.2.3