MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4448 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 10 deletions

diff --git a/dev/translate.txt b/dev/translate.txt
index 6017f39d4a..9dfe9ca1bb 100644
--- a/dev/translate.txt
+++ b/dev/translate.txt
@@ -47,16 +47,28 @@ associativity of an operator cannot be redefined. Typical level are:
 
   The new scale can induce incompatibilities. To set the level an
 operator should have after translation, use the V8only modifier of
-Infix or Notation in the v7 file (V8only not supported for Distfix,
+Infix or Notation in the v7 file (V8only is not supported for Distfix,
 use Notation instead), as e.g.:
 
-   Infix 6 "<=" le  V8only 50.
+   Infix 6 "<=" le V8only (at level 50, no associativity).
    Notation "( x , y )" := (pair ? ? x y)  V8only "x , y" (at level 0).
-   Infix 3 "*" mult : nat_scope  V8only (left associativity).
+   Infix 3 "*" mult : nat_scope  V8only (at level 30, left associativity).
 
-  The default for precedence is to multiply the level by 10. Notice
-that you can change not only the precedence but also the
-associativity and the syntax itself.
+  The semantics of V8only is:
+
+  - Without V8only, the associativity is as for V7 and the levels are
+  the V7 levels scaled by 10.
+
+  - If the syntactic parameters of the notation are already defined
+  (e.g. in theories/Init/Notations.v), then the V8only keyword alone
+  means that the levels and associativity will be inherited from the
+  reserved ones for this syntax. No levels and associativity will be
+  mentioned in the v8 files.
+
+  - Otherwise, both associativity and levels must be mentioned after
+  the V8only keyword
+
+  Notice that you can also change the syntax itself.
 
 III) Main examples for new syntax
      ----------------------------
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 9d18cfc913..5ce975e04b 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -187,7 +187,8 @@ Note that \TERM{struct} is not a reserved identifier.
           &&\RNAME{if-case}
 \SEPDEF
 \DEFNT{appl-arg}
-       \KWD{@}~\NT{int}~\!\KWD{:=}~\NTL{constr}{9}  &&\RNAME{impl-arg}
+%       \KWD{@}~\NT{int}~\!\KWD{:=}~\NTL{constr}{9}  &&\RNAME{impl-arg}
+       \KWD{(}~\NT{ident}~\!\KWD{:=}~\NTL{constr}~\KWD{)}  &&\RNAME{impl-arg}
 \nlsep \NTL{constr}{9}
 \SEPDEF
 \DEFNT{atomic-constr}
@@ -846,8 +847,7 @@ $$
        ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr}
 \nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}~\TERM{[}~\STAR{\NT{int}}~\TERM{]}
 \nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}
-\nlsep \TERM{Implicit}~\TERM{Variable}~\KWD{Type}~\PLUS{\NT{ident}}
-       ~\KWD{:}~\NT{constr}
+\nlsep \TERM{Implicit}~\KWD{Type}~\PLUS{\NT{ident}}~\KWD{:}~\NT{constr}
 \SEPDEF
 \DEFNT{command}
        \TERM{Comments}~\STAR{\NT{comment}}
@@ -1047,7 +1047,7 @@ $$
        ~\OPT{\NT{in-scope}}
 \nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr}
        ~\OPT{\NT{modifiers}}~\OPT{\NT{in-scope}}
-\nlsep \TERM{Uninterpreted}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}
+\nlsep \TERM{Reserved}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string}
        ~\OPT{\NT{modifiers}}
 \SEPDEF
 \DEFNT{modifiers}