From 0fd6d57c78e3156a092984bc29ff63aafc8ea6eb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Feb 2004 13:01:00 +0000
Subject: Eviter la stricte redondance de regles de grammaires v7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5395 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 50e3f62607..a75ca26bd2 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -736,7 +736,8 @@ let cache_syntax_extension (_,(_,(prec,prec8),ntn,gr,se)) =
 	Options.if_verbose
 	  warning ("Notation "^ntn^
 	  " was already assigned a different level or sublevels");
-      Egrammar.extend_grammar (Egrammar.Notation (out_some gr))
+      if oldprec = None or out_some oldprec <> out_some prec then
+        Egrammar.extend_grammar (Egrammar.Notation (out_some gr))
     end
   with Not_found ->
     (* Reserve the notation level *)
-- 
cgit v1.2.3