diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-14 11:52:09 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-14 11:52:09 +0000 |
| commit | fddeb98a7238da23f7b4f1019ee1f22f936935eb (patch) | |
| tree | 65635d22c5b245f0b30834a482e8b6c7f693cb03 /toplevel/metasyntax.ml | |
| parent | 536fc9c7ed00a3d8db50c52934eaeeea619c3b13 (diff) | |
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
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a1b42f7be..18dc7366b 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 *) |