From f1541b5c15cc5b6db889cefc18a808d018dad95f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Oct 2000 09:37:20 +0000
Subject: Changement des analyseurs syntaxiques de Grammar et Syntax

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@754 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/omega/OmegaSyntax.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
index 4028a1efba..327f23a644 100644
--- a/contrib/omega/OmegaSyntax.v
+++ b/contrib/omega/OmegaSyntax.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Grammar vernac vernac :=
+Grammar vernac vernac : Ast :=
   omega_sett [ "Set" "Omega" "Time" "." ] -> [(OmegaFlag "+time")]
 | omega_sets [ "Set" "Omega" "System" "." ] -> [(OmegaFlag "+system")]
 | omega_seta [ "Set" "Omega" "Action" "." ] -> [(OmegaFlag "+action")]
@@ -21,8 +21,8 @@ Grammar vernac vernac :=
 | omega_set  [ "Set" "Omega" stringarg($id) "." ] -> [(OmegaFlag $id)].
 
 
-Grammar tactic simple_tactic :=
+Grammar tactic simple_tactic : Ast :=
   omega [ "Omega" ] -> [(Omega)].
 
 Syntax tactic level 0:
-  omega [(Omega)] -> ["Omega"].
+  omega [ << (Omega) >> ] -> ["Omega"].
-- 
cgit v1.2.3