From fddeb98a7238da23f7b4f1019ee1f22f936935eb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 14 Oct 2003 11:52:09 +0000
Subject: En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est
 pas une erreur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4635 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a1b42f7bea..18dc7366b5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -657,12 +657,16 @@ let pr_level ntn (from,args) =
 let cache_syntax_extension (_,(_,(prec,prec8),ntn,gr,se)) =
   try 
     let oldprec, oldprec8 = Symbols.level_of_notation ntn in
-    if prec8 <> oldprec8 then errorlabstrm ""
-      (str ((if Options.do_translate () then "For new syntax, notation " else "Notation ")
-       ^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec8 ++ spc() 
-      ++ str "while it is now required to be" ++ spc() ++ 
-      pr_level ntn prec8)
+    if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then
+      errorlabstrm ""
+	(str ((if Options.do_translate () then "For new syntax, notation "
+	else "Notation ")
+	^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec8 ++ 
+	spc() ++ str "while it is now required to be" ++ spc() ++ 
+	pr_level ntn prec8)
     else
+      (* Inconsistent v8 notations but not while translating; forget... *)
+      ();
     (* V8 notations are consistent (from both translator or v8) *)
     if prec <> None then begin
       (* Update the V7 parsing rule *)
-- 
cgit v1.2.3