From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 parsing/g_vernac.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'parsing/g_vernac.ml4')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b2d67e1c..f727dfea 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id: g_vernac.ml4 13197 2010-06-25 22:36:17Z letouzey $ *)
 
 
 open Pp
@@ -663,6 +663,8 @@ GEXTEND Gram
   check_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
           fun g -> VernacCheckMayEval (Some r, g, c)
+      | IDENT "Compute"; c = lconstr ->
+	  fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c)
       | IDENT "Check"; c = lconstr ->
 	  fun g -> VernacCheckMayEval (None, g, c) ] ]
   ;
-- 
cgit v1.2.3