From aa9004866904af3a4f6fdfe6fe2efb97c74a89d2 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 5 Dec 2000 22:14:10 +0000
Subject: Plus de quote devant les ident et les ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1054 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7cdf643980..621314137b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -294,6 +294,10 @@ GEXTEND Gram
     [ [ "()" -> <:ast< (VOID) >>
       | n = pure_numarg -> n
       |	id = identarg -> id
+      |	"?" -> <:ast< (COMMAND (ISEVAR)) >>
+      | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >>
+      |	IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
+        <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
       |	"'"; c = constrarg ->
           (match c with
            | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>>
-- 
cgit v1.2.3