Notation 2:Check et 2:Eval

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

1 files changed, 11 insertions, 1 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c9a0d69c7..146bce48d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -39,11 +39,21 @@ GEXTEND Gram
       | g = gallina_ext; "." -> g
       | c = command; "." -> c 
       | c = syntax; "." -> c
-      | n = Prim.natural; ":"; tac = Tactic.tactic; "." -> VernacSolve (n,tac)
+      | n = Prim.natural; ":"; v = goal_vernac; "." -> v n
       | "["; l = vernac_list_tail -> VernacList l
       (* This is for "Grammar vernac" rules *)
       | id = Prim.metaident -> VernacVar (Ast.nvar_of_ast id) ] ]
   ;
+  goal_vernac:
+    [ [ tac = Tactic.tactic -> fun n -> VernacSolve (n,tac)
+      | v = check_command -> fun n -> v (Some n) ] ]
+  ;
+  check_command:
+    [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = constr ->
+          fun g -> VernacCheckMayEval (Some r, g, c)
+      | IDENT "Check"; c = constr ->
+	  fun g -> VernacCheckMayEval (None, g, c) ] ]
+  ;
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
   ;