*** empty log message ***

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

1 files changed, 532 insertions, 60 deletions

diff --git a/doc/Translator.tex b/doc/Translator.tex
index 49c42d080..fb2effc01 100644
--- a/doc/Translator.tex
+++ b/doc/Translator.tex
@@ -35,27 +35,73 @@
    \begin{tabular}[t]{@{}l@{}}#2\end{tabular} & #3 \\}
 
 %%
+%%
+%%
 \begin{document}
 \maketitle
 
 \section{Introduction}
 
-The goal of this document is to introduce to the new syntax of Coq on
+Coq version 8.0 is a major version and carries major changes: the
+concrete syntax was redesigned almost from scratch, and many notions
+of the libraries were renamed for uniformisation purposes. We felt
+that these changes could discourage users with large theories from
+switching to the new version.
+
+The goal of this document is to introduce these changes on simple
+examples (mainly the syntactic changes), and describe the automated
+tools to help moving to V8.0. Essentially, it consists of a translator
+that takes as input a Coq source file in old syntax and produces a
+file in new syntax and adapted to the new standard library. The main
+extra features of this translator is that it keeps comments, even
+those within expressions\footnote{The position of those comment might
+differ slightly since there is no exact matching of positions between
+old and new syntax.}.
+
+The document is organised as follows: first section describes the new
+syntax on simple examples. It is very translation-oriented. This
+should give users of older versions the flavour of the new syntax, and
+allow them to make translation manually on small
+examples. Section~\ref{Translation} explains how the translation
+process can be automatised for the most part (the boring one: applying
+similar changes over thousands of lines of code). We strongly advise
+users to follow these indications, in order to avoid many potential
+complications of the translation process.
+
+
+\section{The new syntax on examples}
+
+The goal of this section is to introduce to the new syntax of Coq on
 simple examples, rather than just giving the new grammar. It is
 strongly recommended to read first the definition of the new syntax
 (in the reference manual), but this document should also be useful for
 the eager user who wants to start with the new syntax quickly.
 
-\section{The new syntax on examples}
-
 The toplevel has an option {\tt -translate} which allows to
-interactively translate commands. All the examples below can be tested
-by entering the V7 commands in the toplevel launched this option. This
-toplevel translator accepts a command, prints the translation on
-standard output (after a \verb+New syntax:+ balise), executes the
-command, and waits for another command. The only requirements is that
-they should be syntactically correct, but they do not have to be
-well-typed.
+interactively translate commands. This toplevel translator accepts a
+command, prints the translation on standard output (after a \verb+New
+syntax:+ balise), executes the command, and waits for another
+command. The only requirements is that they should be syntactically
+correct, but they do not have to be well-typed.
+
+This interactive translator proved to be useful in two main
+usages. First as a ``debugger'' of the translation. Before the
+translation, it may help in spotting possible conflicts between the
+new syntax and user notations. Or when the translation fails for some
+reason, it makes it easy to find the exact reason why it failed and
+make attempts in fixing the problem.
+
+The second usage of the translator is when trying to make the first
+proofs in new syntax. Well trained users will automatically think
+their scripts in old syntax and might waste much time (and the
+intuition of the proof) if they have to search the translation in a
+document. Running a translator in the background will allow the user
+to instantly have the answer.
+
+The rest of this section is a description of all the aspects of the
+syntax that changed and how they were translated. All the examples
+below can be tested by entering the V7 commands in the toplevel
+translator.
 
 %%
 
@@ -77,6 +123,12 @@ be a regular identifier). As before they are written between double
 quotes ("). Unlike for V7, there is no escape character: characters
 are written normaly but the double quote which is doubled.
 
+\begin{transbox}
+\TRANS{"abcd$\backslash\backslash$efg"}{"abcd$\backslash$efg"}
+\TRANS{"abcd$\backslash$"efg"}{"abcd""efg"}
+\end{transbox}
+
+
 \subsection{Main changes in terms w.r.t. V7}
 
 
@@ -112,7 +164,11 @@ types & type_scope & \TERM{type} \\
 \end{tabular}
 \end{center}
 
-In order to use notations of arithmetics on \TERM{Z}, its scope must be opened with command \verb+Open Scope Z_scope.+ Another possibility is using the scope change notation (\TERM{\%}). The latter notation is to be used when notations of several scopes appear in the same expression.
+In order to use notations of arithmetics on \TERM{Z}, its scope must
+be opened with command \verb+Open Scope Z_scope.+ Another possibility
+is using the scope change notation (\TERM{\%}). The latter notation is
+to be used when notations of several scopes appear in the same
+expression.
 
 In examples below, scope changes are not needed if the appropriate scope
 has been opened. Scope nat_scope is opened in the initial state of Coq.
@@ -147,10 +203,10 @@ list_scope & $\TERM{::} ~\TERM{++}$
 
 \subsubsection{Notation for implicit arguments}
 
-The explicitation of arguments is closer to the \emph{bindings} notation in
-tactics. Argument positions follow the argument names of the head
-constant. The example below assumes \verb+f+ is a function with 2
-dependent arguments named \verb+x+ and \verb+y+, and a third
+The explicitation of arguments is closer to the \emph{bindings}
+notation in tactics. Argument positions follow the argument names of
+the head constant. The example below assumes \verb+f+ is a function
+with 2 dependent arguments named \verb+x+ and \verb+y+, and a third
 non-dependent argument.
 \begin{transbox}
 \TRANS{f 1!t1 2!t2 3!t3}{f (x:=t1) (y:=t2) (1:=t3)}
@@ -158,6 +214,15 @@ non-dependent argument.
 \end{transbox}
 
 
+\subsubsection{Inferred subterms}
+
+Subterms that can be automatically inferred by the type-checker is now
+written {\tt _}
+
+\begin{transbox}
+\TRANS{?}{_}
+\end{transbox}
+
 \subsubsection{Universal quantification}
 
 The universal quantification and dependent product types are now
@@ -196,23 +261,43 @@ Beside the usage of the keyword pair \TERM{match}/\TERM{with} instead of
 branches and return type. It is no longer written between \TERM{$<$ $>$} before
 the \TERM{Cases} keyword, but interleaved with the destructured objects.
 
-The idea is that for each destructured object, one may specify a variable
-name to tell how the branches types depend on this destructured objects (case
-of a dependent elimination), and also how they depend on the value of the
-arguments of the inductive type of the destructured objects. The type of
-branches is then given after the keyword \TERM{return}, unless it can be
-inferred.
+The idea is that for each destructured object, one may specify a
+variable name (after the \TERM{as} keyword) to tell how the branches
+types depend on this destructured objects (case of a dependent
+elimination), and also how they depend on the value of the arguments
+of the inductive type of the destructured objects (after the \TERM{in}
+keyword). The type of branches is then given after the keyword
+\TERM{return}, unless it can be inferred.
 
 Moreover, when the destructured object is a variable, one may use this
 variable in the return type.
 
 \begin{transbox}
-\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| (S k) => 1 end}
-\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| .. end}
+\TRANS{Cases n of\\~~ O => O \\| (S k) => (1) end}{match n with\\~~ 0 => 0 \\| S k => 1 end}
+\TRANS{Cases m n of \\~~0 0 => t \\| ... end}{match m, n with \\~~0, 0 => t \\| ... end}
 \TRANS{<[n:nat](P n)>Cases T of ... end}{match T as n return P n with ... end}
 \TRANS{<[n:nat][p:(even n)]\~{}(odd n)>Cases p of\\~~ ... \\end}{match p in even n return \~{} odd n with\\~~ ...\\end}
 \end{transbox}
 
+The annotations of the special pattern-matching operators
+(\TERM{if}/\TERM{then}/\TERM{else}) and \TERM{let()} also changed. The
+only restriction is that the destructuring \TERM{let} does not allow
+dependent case analysis.
+
+\begin{transbox}
+\TRANS{
+ \begin{tabular}{@{}l}
+ <[n:nat;x:(I n)](P n x)>if t then t1 \\
+ else t2
+ \end{tabular}}%
+{\begin{tabular}{@{}l}
+ if t as x in I n return P n x then t1 \\
+ else t2
+ \end{tabular}}
+\TRANS{<[n:nat](P n)>let (p,q) = t1 in t2}%
+{let (p,q) in I n return P n := t1 in t2}
+\end{transbox}
+
 
 \subsubsection{Fixpoints and cofixpoints}
 
@@ -250,11 +335,25 @@ The same applies to cofixpoints, annotations are not allowed in that case.
 The main change is that all tactic names are lowercase. This also holds for
 Ltac keywords.
 
+\subsubsection{Renaming of tactics}
+
+\begin{transbox}
+\TRANS{NewDestruct}{destruct}
+\TRANS{NewInduction}{induction}
+\TRANS{Induction}{simple induction}
+\TRANS{Destruct}{simple destruct}
+\end{transbox}
+
 \subsubsection{Ltac}
 
 Definitions of macros are introduced by \TERM{Ltac} instead of
 \TERM{Tactic Definition}, \TERM{Meta Definition} or \TERM{Recursive
-Definition}.
+Definition}. They are considered recursive by default.
+
+\begin{transbox}
+\TRANS{Meta Definition my_tac t1 t2 := t1; t2.}%
+{Ltac my_tac t1 t2 := t1; t2.}
+\end{transbox}
 
 Rules of a match command are not between square brackets anymore.
 
@@ -262,9 +361,25 @@ Context (understand a term with a placeholder) instantiation \TERM{inst}
 became \TERM{context}. Syntax is unified with subterm matching.
 
 \begin{transbox}
-\TRANS{match t with [C[x=y]] => inst C[y=x]}{match t with context C[x=y] => context C[y=x]}
+\TRANS{Match t With [C[x=y]] -> Inst C[y=x]}%
+{match t with context C[x=y] => context C[y=x] end}
 \end{transbox}
 
+Arguments of macros use the term syntax. If a general Ltac expression
+is to be passed, it must be prefixed with ``{\tt ltac :}''. In other
+cases, when a \'{} was necessary, it is replaced by ``{\tt constr :}''
+
+\begin{transbox}
+\TRANS{my_tac '(S x)}{my_tac (S x)}
+\TRANS{my_tac (Let x=tac In x)}{my_tac ltac:(let x:=tac in x)}
+\TRANS{Let x = '[x](S (S x)) In Apply x}%
+{let x := constr:(fun x => S (S x)) in apply x}
+\end{transbox}
+
+{\tt Match Context} is now called {\tt match goal}. Its argument is an
+Ltac by default.
+
+
 \subsubsection{Named arguments of theorems ({\em bindings})}
 
 \begin{transbox}
@@ -276,13 +391,44 @@ became \TERM{context}. Syntax is unified with subterm matching.
 
 To avoid ambiguity between a numeric literal and the optionnal
 occurence numbers of this term, the occurence numbers are put after
-the term itself and after keyword \TERM{as}. This applies to tactic
-\TERM{pattern} and also
-\TERM{unfold}
+the term itself and after keyword \TERM{as}.
+\begin{transbox}
+\TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern f x at 1 2, d at 3 4, y, z}
+\end{transbox}
+
+
+\subsubsection{{\tt LetTac} and {\tt Pose}}
+
+Tactic {\tt LetTac} was renamed into {\tt set}, and tactic {\tt Pose}
+was a particular case of {\tt LetTac}\footnote{There is a tactic
+called {\tt pose} in V8, but its behaviour is not to fold the
+abbreviation.}.
+
 \begin{transbox}
-\TRANS{Pattern 1 2 (f x) 3 4 d y z}{pattern (f x at 1 2) (d at 3 4) y z}
+\TRANS{LetTac x = t in H}{set (x := t) in H}
+\TRANS{Pose x := t}{set (x := t)}
 \end{transbox}
 
+{\tt LetTac} could be followed by a specification (called a clause) of
+the hypotheses where the abbreviation had to be folded (and also if it
+should occur in the conclusion). Clauses are the syntactic notion to
+denote in which parts of a goal a given transformation shold
+occur. Its basic notation is either \TERM{*} (meaning everywhere), or
+{\tt\textrm{\em hyps} |- \textrm{\em concl}} where {\em hyps} is
+either \TERM{*} (to denote all the hypotheses), or a comma-separated
+list of either hypothesis name, or {\tt (value of $H$)} or {\tt (type
+of $H$)}. Moreover, occurrences can be specified after every
+hypothesis after the {\TERM{at}} keyword. {\em concl} is either empty
+or \TERM{*}, and can be followed by occurences.
+
+\begin{transbox}
+\TRANS{in Goal}{in |- *}
+\TRANS{in H H1}{in H1, H2 |-}
+\TRANS{in H H1 ...}{in * |-}
+\TRANS{in H H1 Goal}{in H1, H2 |- *}
+\TRANS{in H H1 H2 ... Goal}{in *}
+\TRANS{in 1 2 H 3 4 H0 1 3 Goal}{in H at 1 2, H0 at 3 4 |- * at 1 3}
+\end{transbox}
 
 \subsection{Main changes in vernacular commands w.r.t. V7}
 
@@ -299,43 +445,152 @@ fixpoints. This also holds for parameters of inductive definitions.
       {Inductive and (A B:Prop): Prop := \\~~conj : A -> B -> and A B}
 \end{transbox}
 
+\subsubsection{Require}
+
+The default behaviour of {\tt Require} is not to open the loaded
+module.
+
+\begin{transbox}
+\TRANS{Require Arith}{Require Import Arith}
+\end{transbox}
+
 \subsubsection{Hints}
 
-The syntax of \emph{extern} hints changed: the pattern and the tactic
+Names of hints are not supported anymore, except for {\tt HintDestruct}.
+
+The syntax of \emph{Extern} hints changed: the pattern and the tactic
 to be applied are separated by a \TERM{$\Rightarrow$}.
 \begin{transbox}
-\TRANS{Hint Extern 4 (toto ?) Apply lemma}{Hint Extern 4 (toto _) => apply lemma}
+\TRANS{Hint name := Resolve (f ? x)}%
+{Hint Resolve (f _ x)}
+\TRANS{Hint name := Extern 4 (toto ?) Apply lemma}%
+{Hint Extern 4 (toto _) => apply lemma}
+\TRANS{Hints Resolve x y z}{Hint Resolve x y z}
+\TRANS{Hints Resolve f : db1 db2}{Hint Resolve f : db1 db2}
+\TRANS{Hints Immediate x y z}{Hint Immediate x y z}
+\TRANS{Hints Unfold x y z}{Hint Unfold x y z}
+\TRANS{\begin{tabular}{@{}l}
+  HintDestruct Local Conclusion \\
+  ~~name (f ? ?) 3 [Apply thm]
+  \end{tabular}}%
+{\begin{tabular}{@{}l}
+ Hint Local Destuct name := \\
+ ~~3 Conclusion (f _ _) => apply thm
+ \end{tabular}}
+\end{transbox}
+
+
+\subsubsection{Implicit arguments}
+
+
+{\tt Set Implicit Arguments} changed its meaning in V8: the default is
+to turn implicit only the arguments that are {\em strictly} implicit
+(or rigid), i.e. that remains inferable whatever the other arguments
+are. For instance {\tt x} inferable from {\tt P x} is not strictly
+inferable since it can disappears if {\tt P} is instanciated by a term
+which erases {\tt x}.
+
+\begin{transbox}
+\TRANS{Set Implicit Arguments}%
+{\begin{tabular}{l}
+ Set Implicit Arguments. \\
+ Unset Strict Implicits.
+ \end{tabular}}
+\end{transbox}
+
+However, you may wish to adopt the new semantics of {\tt Set Implicit
+Arguments} (for instance because you think that the choice of
+arguments it sets implicit is more ``natural'' for you).
+
+
+\subsection{Changes in standard library}
+
+Many lemmas had their named changed to improve uniformity. The user
+generally do not have to care since the translators performs the
+renaming.
+
+  Type {\tt entier} from fast_integer.v is renamed into {\tt N} by the
+translator. As a consequence, user-defined objects of same name {\tt N}
+are systematically qualified even tough it may not be necessary.  The
+following table lists the main names with which the same problem
+arises:
+\begin{transbox}
+\TRANS{IF}{IF_then_else}
+\TRANS{ZERO}{Z0}
+\TRANS{POS}{Zpos}
+\TRANS{NEG}{Zneg}
+\TRANS{SUPERIEUR}{Gt}
+\TRANS{EGAL}{Eq}
+\TRANS{INFERIEUR}{Lt}
+\TRANS{add}{Pplus}
+\TRANS{true_sub}{Pminus}
+\TRANS{entier}{N}
+\TRANS{Un_suivi_de}{Ndouble_plus_one}
+\TRANS{Zero_suivi_de}{Ndouble
+\TRANS{Nul}{N0}
+\TRANS{Pos}{Npos}
 \end{transbox}
 
 
+\subsubsection{Implicit arguments}
+
+%% Hugo: 
+Main definitions of standard library have now implicit
+arguments. These arguments are dropped in the translated files. This
+can exceptionally be a source of incompatibilities which has to be
+solved by hand (it typically happens for polymorphic functions applied
+to {\tt nil} or {\tt None}).
+%% preciser: avant ou apres trad ?
+
+\subsubsection{Logic about {\tt Type}}
+
+Many notations that applied to {\tt Set} have been extended to {\tt
+Type}, so several definitions in {\tt Type} are superseded by them.
+
+\begin{transbox}
+\TRANS{x==y}{x=y}
+\TRANS{(EXT x:Prop | Q)}{exists x:Prop, Q}
+\TRANS{identityT}{identity}
+\end{transbox}
+
 
 
 %% Doc of the translator
 \section{A guide to translation}
+\label{Translation}
 
 \subsection{Overview of the translation process}
 
-Tools:
-\begin{itemize}
-\item {\tt coqc -translate}
+Here is a short description of the tools of the translation package:
+\begin{description}
+\item{\tt coqc -translate}
 is the automatic translator. It is a parser/pretty-printer. This means
 that the translation is made by parsing using a parser of old syntax,
 and every command is printed using the new syntax. Many efforts were
 made to preserve as much as possible the quality of the presentation:
 it avoids expansion of syntax extensions, comments are not discarded
 and placed at the same place.
-\item {\tt tools/translate-v8} will help translate developments that
-compile with a Makefile with minimum requirements.
-\end{itemize}
+\item{\tt tools/translate-v8} is a small shell-script that will help
+translate developments that compile with a Makefile with minimum
+requirements.
+\end{description}
 
-\subsection{What to do before the translation}
+\subsection{Preparation to translation}
+
+This step is very important because most of work shall be done before
+translation. If a problem occurs during translation, it often means
+that you will have to modify the original source and restart the
+translation process.
+
+\subsubsection{Compilation with {\tt coqc -v7}}
 
 First of all, it is mandatory that files compile with the current
-version of Coq with option {\tt -v7}. Translation is a complicated
-task that involves the full compilation of the development. If your
-development was compiled with older versions, first upgrade to Coq V8
-with option {\tt -v7}. If you use a Makefile similar to those produced
-by {\tt coq\_makefile}, you probably just have to do
+version of Coq (8.0) with option {\tt -v7}. Translation is a
+complicated task that involves the full compilation of the
+development. If your development was compiled with older versions,
+first upgrade to Coq V8.0 with option {\tt -v7}. If you use a Makefile
+similar to those produced by {\tt coq\_makefile}, you probably just
+have to do
 
 {\tt make OPT="-opt -v7"} ~~~or~~~ {\tt make OPT="-byte -v7"}
 
@@ -345,10 +600,14 @@ about syntax extensions (see section below dedicated to porting syntax
 extensions). If you do not use such features, then you are ready to
 try and make the translation.
 
+\subsection{Translation}
+
+\subsubsection{The general case}
+
 The preferred way is to use script {\tt translate-v8} if your development
 is compiled by a Makfile with the following constraints:
 \begin{itemize}
-\item compilation is achievd by invoke make without arguments
+\item compilation is achievd by invoke make without specifying a target
 \item options are passed to Coq with make variable COQFLAGS that
   includes variables OPT, COQLIBS, OTHERFLAGS and COQ_XML.
 \end{itemize}
@@ -360,20 +619,49 @@ ouptut the translated source of any {\tt .v} file in a file with
 extension {\tt .v8} located in the same directory than the original
 file.
 
-The following section describes events that may happen during the
-translation and measures to adopt.
+\subsubsection{What may happen during the translation}
 
-\subsection{What may happens during the translation}
+This section describes events that may happen during the
+translation and measures to adopt.
 
+These are the warnings that may arise during the translation, but they
+generally do not require any modification for the user:
 Warnings:
+\begin{itemize}
+\item {\tt Unable to detect if $id$ denotes a local definition}\\
+This is due to a semantic change in clauses. In a command such as {\tt
+simpl in H}, the old semantics were to perform simplification in the
+type of {\tt H}, or in its body if it is defined. With the new
+semantics, it is performed both in the type and the body (if any). It
+might lead to incompatibilities
+
+\item {\tt Forgetting obsolete module}\\
+Some modules have disappeared in V8.0 (new syntax). The user does not
+need to worry about it, since the translator deals with it.
+
+\item {\tt Replacing obsolete module}\\
+Same as before but with the module that were renamed. Here again, the
+translator deals with it.
+\end{itemize}
 
-...
-
-\subsection{Errors occurring after translation}
+\subsection{Verification of the translation}
 
-Equality in {\tt Z} or {\tt R}...
+The shell-script {\tt translate-v8} also renames {\tt .v8} files into
+{\tt .v} files (older {\tt .v} files are put in a subdirectory called
+{\tt v7}) and tries to recompile them. To do so it invokes {\tt make}
+without option (which should cause the compilation using {\tt coqc}
+without particular option).
 
+If compilation fails at this stage, you should refrain from repairing
+errors manually on the new syntax, but rather modify the old syntax
+script and restart the translation. We insist on that because the
+problem encountered can show up in many instances (especially if the
+problem comes from a syntactic extension), and fixing the original
+sources (for instance the {\tt V8only} parts of notations) once will
+solve all occurrences of the problem.
 
+%%\subsubsection{Errors occurring after translation}
+%%Equality in {\tt Z} or {\tt R}...
 
 \subsection{Particular cases}
 
@@ -395,20 +683,21 @@ If the choices made by translation or in the following cases:
 the user should change his development prior to translation.
 
 
-\subsubsection{Syntax extensions}
+\subsubsection{{\tt Case} and {\tt Match}}
 
-\paragraph{Notation and Infix}
+These very low-level case analysis are no longer supported. The
+translator tries hard to translate them into a user-friendly one, but
+it might lack type information to do so\footnote{The translator tries
+to typecheck terms before printing them, but it is not always possible
+to determine the context in which terms appearing in tactics
+live.}. If this happens, it is preferable to transform it manually
+before translation.
 
-These commands do not necessarily need to be changed.
-
-Some work will have to be done manually if the notation conflicts with
-the new syntax (for instance, using keywords like {\tt fun} or {\tt
-exists}, overloading of symbols of the old syntax).
 
+\subsubsection{Syntax extensions with {\tt Grammar} and {\tt Syntax}}
 
-\paragraph{Grammar and Syntax}
 
-{\tt Grammar} and {\tt Syntax} are not supported by translation. They
+{\tt Grammar} and {\tt Syntax} are no longer supported. They
 should be replaced by an equivalent {\tt Notation} command and be
 processed as decribed above. Before attempting translation, users
 should verify that compilation with option {\tt -v7} succeeds.
@@ -419,5 +708,188 @@ they wish to avoid the use of {\tt Grammar}. If this is not done, the
 translator will simply expand the notations and the output of the
 translator will use the reuglar Coq syntax.
 
+\subsubsection{Syntax extensions with {\tt Notation} and {\tt Infix}}
+
+These commands do not necessarily need to be changed.
+
+Some work will have to be done manually if the notation conflicts with
+the new syntax (for instance, using keywords like {\tt fun} or {\tt
+exists}, overloading of symbols of the old syntax, etc.) or if the
+precedences are not right.
+
+  Precedence levels are now from 0 to 200. In V8, the precedence and
+associativity of an operator cannot be redefined. Typical level are
+(refer to the chapter on notations in the Reference Manual for the
+full list):
+
+\begin{center}
+\begin{tabular}{|cll|}
+\hline
+Notation & Precedence & Associativity \\
+\hline
+\verb!_ <-> _! & 95 & no \\
+\verb!_ \/ _!  & 85 & right \\
+\verb!_ /\ _!  & 80 & right \\
+\verb!~ _!   & 75 & right \\
+\verb!_ = _!, \verb!_ <> _!, \verb!_ < _!, \verb!_ > _!,
+  \verb!_ <= _!, \verb!_ >= _!   & 70 & no \\
+\verb!_ + _!, \verb!_ - _!   & 50 & left \\
+\verb!_ * _!, \verb!_ / _!   & 40 & left \\
+\verb!- _!  & 35 & right \\
+\verb!_ ^ _!   & 30 & left \\
+\hline
+\end{tabular}
+\end{center}
+
+
+  By default, the translator keeps the associativity given in V7 while
+the levels are mapped according to the following table:
+ 
+\begin{center}
+\begin{tabular}{l|l|l}
+V7 level & mapped to & associativity \\
+\hline
+0 & 0 & no \\
+1 & 20 & left \\
+2 & 30 & right \\
+3 & 40 & left \\
+4 & 50 & left \\
+5 & 70 & no \\
+6 & 80 & right \\
+7 & 85 & right \\
+8 & 90 & right \\
+9 & 95 & no \\
+10 & 100 & left
+\end{tabular}
+\end{center}
+
+If this is OK, just simply apply the translator.
+
+
+\paragraph{Associativity conflict}
+
+  Since the associativity of the levels obtained by translating a V7
+level (as shown on table above) cannot be changed, you have to choose
+another level with a compatible associativity.
+
+  You can choose any level between 0 and 200, knowing that the
+standard operators are already set at the levels shown on the list
+above. 
+
+Assume you have a notation
+\begin{verbatim}
+Infix NONA 2 "=_S" my_setoid_eq.
+\end{verbatim}
+By default, the translator moves it to level 30 which is right
+associative, hence a conflict with the expected no associativity.
+
+To solve the problem, just add the "V8only" modifier to reset the
+level and enforce the associativity as follows:
+\begin{verbatim}
+Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
+\end{verbatim}
+The translator now knows that it has to translate "=_S" at level 70
+with no associativity.
+
+Remark: 70 is the "natural" level for relations, hence the choice of 70
+here, but any other level accepting a no-associativity would have been
+OK.
+
+Second example: assume you have a notation
+\begin{verbatim}
+Infix RIGHTA 1 "o" my_comp.
+\end{verbatim}
+By default, the translator moves it to level 20 which is left
+associative, hence a conflict with the expected right associativity.
+
+To solve the problem, just add the "V8only" modifier to reset the
+level and enforce the associativity as follows:
+\begin{verbatim}
+Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
+\end{verbatim}
+The translator now knows that it has to translate "o" at level 20
+which has the correct "right associativity".
+
+Remark: we assumed here that the user wants a strong precedence for
+composition, in such a way, say, that "f o g + h" is parsed as
+"(f o g) + h". To get "o" binding less than the arithmetical operators,
+an appropriated level would have been close of 70, and below, e.g. 65.
+
+
+\paragraph{Conflict: notation hides another notation}
+
+Remark: use {\tt Print Grammar constr} in V8 to diagnose the overlap
+and see the section on factorization in the chapter on notations of
+the Reference Manual for hints on how to factorize.
+
+Example:
+\begin{verbatim}
+Notation "{ x }" := (my_embedding x) (at level 1).
+\end{verbatim}
+overlaps in V8 with notation \verb#{ x : A & P }# at level 0 and with
+x at level 99. The conflicts can be solved by left-factorizing the
+notation as follows:
+\begin{verbatim}
+Notation "{ x }" := (my_embedding x) (at level 1)
+  V8only (at level 0, x at level 99).
+\end{verbatim}
+
+\paragraph{Confilct: a notation conflicts with the V8 grammar}
+
+Again, use the {\tt V8only} modifier to tell the translator to
+automatically take in charge the new syntax.
+
+Example:
+\begin{verbatim}
+Infix 3 "@" app.
+\end{verbatim}
+Since {\tt @} is used in the new syntax for deactivating the implicit
+arguments, another symbol has to be used, e.g. {\tt @@}. This is done via
+the {\tt V8only} option as follows:
+\begin{verbatim}
+Infix 3 "@" app V8only "@@" (at level 40, left associativity).
+\end{verbatim}
+or, alternatively by
+\begin{verbatim}
+Notation "x @ y" := (app x y) (at level 3, left associativity)
+  V8only "x @@ y" (at level 40, left associativity).
+\end{verbatim}
+
+\paragraph{Conflict: my notation is already defined at another level
+  (or with another associativity)}
+
+In V8, the level and associativity of a given notation can no longer
+be changed. Then, either you adopt the standard reserved levels and
+associativity for this notation (as given on the list above) or you
+change your notation.
+\begin{itemize}
+\item To change the notation, follow the directions in the previous
+paragraph
+\item To adopt the standard level, just use {\tt V8only} without any
+argument.
+\end{itemize}
+
+Example:
+\begin{verbatim}
+Infix 6 "*" my_mult.
+\end{verbatim}
+is not accepted as such in V8. Write
+\begin{verbatim}
+Infix 6 "*" my_mult V8only.
+\end{verbatim}
+to tell the translator to use {\tt *} at the reserved level (i.e. 40
+with left associativity). Even better, use interpretation scopes (look
+at the Reference Manual).
+
+
+\subsubsection{Strict implicits}
+
+In the case you want to adopt the new semantics of {\tt Set Implicit
+ Arguments} (only setting rigid arguments implicit), add the option
+{\tt -strict-implicit} to the translator.
+
+Warning: changing the number of implicit arguments can break the
+notations.  Then use the {\tt V8only} modifier of {\tt Notation}.
+
 
 \end{document}