From 503fc133279161abe87ff8329c630126b9b86e35 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 26 Jul 2000 16:29:22 +0000
Subject: Ajout syntaxe [ phr1 ... phrn ]. pour grouper des commandes (pour
 Time ou Grammar)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@574 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES                  | 4 ++++
 parsing/g_basevernac.ml4 | 3 ---
 parsing/g_vernac.ml4     | 8 +++++++-
 3 files changed, 11 insertions(+), 4 deletions(-)

diff --git a/CHANGES b/CHANGES
index 5375923570..9e29a7e502 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,3 +12,7 @@
 - Les cas des Cases ne se lisent plus de manière séquentielle, sauf en
   cas de clauses par défaut redondantes auquel cas la première est prise
   avec un avertissement.
+
+- Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
+phrases (utile pour Time et pour des grammaires abrégeant plusieurs
+commandes)
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 41f0a82d4b..ad1fbd1b55 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -113,9 +113,6 @@ GEXTEND Gram
       | IDENT "Print"; IDENT "Path"; c = identarg; d = identarg; "." ->
           <:ast< (PrintPATH $c $d) >>
 
-(*      | IDENT "Time"; "." -> <:ast< (Time) >>
-      | IDENT "Untime"; "." -> <:ast< (Untime) >> *)
-
       | IDENT "Time"; v = vernac -> <:ast< (Time $v)>>
       | IDENT "SearchIsos"; com = constrarg; "." ->
           <:ast< (Searchisos $com) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f29f4407e0..187c75c073 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -8,15 +8,21 @@ open Util
 open Vernac
 
 GEXTEND Gram
+  GLOBAL: vernac;
   vernac:
     [ [ g = gallina -> g 
       | g = gallina_ext -> g
       | c = command -> c 
-      | c = syntax -> c ] ]
+      | c = syntax -> c
+      | "["; l = vernac_list_tail -> <:ast< (VernacList ($LIST $l)) >> ] ]
   ;
   vernac: LAST
     [ [ tac = tacarg; "." -> <:ast< (SOLVE 1 (TACTIC $tac)) >> ] ]
   ;
+  vernac_list_tail:
+    [ [ v = vernac; l = vernac_list_tail -> v :: l
+      | "]"; "." -> [] ] ]
+  ;
 END
 
 (* Gallina declarations *)
-- 
cgit v1.2.3