From c9aa1b6d908d3a4f8d9906ba0f11c0bb11569ab7 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 5 Feb 2001 18:27:32 +0000
Subject: Correction pour Time pour ne pas etre oblige de mettre deux points

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1326 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_basevernac.ml4 | 1 -
 parsing/g_vernac.ml4     | 3 +++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index def0127333..a310bb15c6 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -154,7 +154,6 @@ GEXTEND Gram
       | IDENT "Print"; IDENT "Coercion"; IDENT "Paths"; c = identarg; d = identarg ->
           <:ast< (PrintPATH $c $d) >>
 
-      | IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
       | IDENT "SearchIsos"; com = constrarg ->
           <:ast< (Searchisos $com) >>
       | "Set"; IDENT "Undo"; n = numarg ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c0b8e45ab0..5f8106f2d0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -23,6 +23,9 @@ GEXTEND Gram
       | c = syntax; "." -> c
       | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ]
   ;
+  vernac: FIRST
+    [ [ IDENT "Time"; v = vernac  -> <:ast< (Time $v)>> ] ]
+  ;
   vernac: LAST
     [ [ tac = tacarg; "." ->
         (match tac with
-- 
cgit v1.2.3