From 34e53d5418fa08e69c8f599bb55a89eae027b9b5 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 27 May 2002 15:35:34 +0000
Subject: Ajout de Eval, Inst et Check

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constr.ml4 | 5 +++--
 parsing/g_ltac.ml4   | 2 ++
 2 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ca5f582d9f..c93acba58b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -56,9 +56,10 @@ GEXTEND Gram
   constr:
     [ [ c = constr8 -> c
       | IDENT "Inst"; id = ident; "["; c = constr8; "]" ->
-        <:ast< (CONTEXT $id $c) >>
+        <:ast<(CONTEXT $id $c)>>
       | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 ->
-        <:ast< (EVAL $c (REDEXP $rtc)) >> ] ]
+        <:ast<(EVAL $c (REDEXP $rtc))>>
+      | IDENT "Check"; c = constr8 -> <:ast<(CHECK $c)>> ] ]
   ;
   lconstr:
     [ [ c = constr10 -> c ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2beb62f243..ec482d43d0 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -145,6 +145,7 @@ GEXTEND Gram
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
       | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
         <:ast< (COMMAND (CONTEXT $id $c)) >>
+      | IDENT "Check"; c = Constr.constr  -> <:ast<(COMMAND (CHECK $c))>>
       |	st = simple_tactic -> st
       | id = lqualid; la = LIST1 tactic_atom0 ->
         <:ast< (APP $id ($LIST $la)) >>
@@ -164,6 +165,7 @@ GEXTEND Gram
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
       | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
         <:ast< (COMMAND (CONTEXT $id $c)) >>
+      | IDENT "Check"; c = Constr.constr  -> <:ast<(COMMAND (CHECK $c))>>
       |	"'"; c = constrarg -> c ] ]
   ;
   lqualid:
-- 
cgit v1.2.3