From ce0742280919c8a607937b6b927c62f16485a593 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 9 Sep 2003 11:44:50 +0000
Subject: Protection traducteur contre meta de Grammar tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4327 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2efdabafc1..e7f4fff8b9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -719,7 +719,7 @@ and intern_tacarg strict ist = function
   | MetaIdArg (loc,s) ->
       (* $id can occur in Grammar tactic... *)
       let id = id_of_string s in
-      if find_ltacvar id ist
+      if find_ltacvar id ist or Options.do_translate()
       then Reference (ArgVar (adjust_loc loc,strip_meta id))
       else error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,l) ->
-- 
cgit v1.2.3