From d61b606668d7507e42d78b8de8a009fc257f4050 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 19 Sep 2001 12:10:01 +0000
Subject: MAJ V7.1

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1993 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/romega/README   | 13 -------------
 contrib/romega/ROmega.v |  2 +-
 2 files changed, 1 insertion(+), 14 deletions(-)

diff --git a/contrib/romega/README b/contrib/romega/README
index c82087c7d3..86c9e58afd 100644
--- a/contrib/romega/README
+++ b/contrib/romega/README
@@ -1,19 +1,6 @@
 This work was done for the RNRT Project Calife. 
 As such it is distributed under the LGPL licence.
 
-Change the COQTOP variable in the Makefile and type make. 
-The caml compiler should be in your path.
-
-WARNING : there is a bug in the 7.0 production release that prevents
-the compilation of the core ReflOmegaCore.v module. This development
-will only work with the beta release and (hopefully) subsequent version
-of Coq.
-
-A patch (patch-v7) contributed by D. Delahaye is included to correct the bug in
-regular 7.0 versions. It must be applied in the 'parsing' directory.
-Using it with a 7.0beta requires a few changes in const_omega.ml due to
-some changes in the paths of modules.
-
 Report bugs to :
   pierre.cregut@francetelecom.com
 
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 2a9dc10070..6bfc3f187a 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -13,5 +13,5 @@ Grammar tactic simple_tactic : ast :=
   romega [ "ROmega" ] -> [(ReflOmega)].
 
 Syntax tactic level 0:
-  romega [ << (ReflOmega) >> ] -> ["ROmega"].   
+  romega [ (ReflOmega) ] -> ["ROmega"].   
      
-- 
cgit v1.2.3