Commit eeb14f3b authored by POTTIER Francois's avatar POTTIER Francois

Document --coq-no-version-check.

parent 201233d8
Pipeline #196777 passed with stages
in 54 seconds
......@@ -94,6 +94,7 @@
\newcommand{\menhir}{Menhir\xspace}
\newcommand{\menhirlib}{\texttt{MenhirLib}\xspace}
\newcommand{\menhirsdk}{\texttt{MenhirSdk}\xspace}
\newcommand{\coqmenhirlib}{\texttt{MenhirLib}\xspace} % for now
\newcommand{\menhirinterpreter}{\texttt{MenhirInterpreter}\xspace}
\newcommand{\cmenhir}{\texttt{menhir}\xspace}
\newcommand{\ml}{\texttt{.ml}\xspace}
......@@ -192,6 +193,7 @@
\newcommand{\ocoqlibnopath}{\oo{coq-lib-no-path}}
\newcommand{\ocoqnocomplete}{\oo{coq-no-complete}}
\newcommand{\ocoqnoactions}{\oo{coq-no-actions}}
\newcommand{\ocoqnoversioncheck}{\oo{coq-no-version-check}}
\newcommand{\olisterrors}{\oo{list-errors}}
\newcommand{\ointerpreterror}{\oo{interpret-error}}
\newcommand{\ocompileerrors}{\oo{compile-errors}}
......
......@@ -130,14 +130,16 @@ irredundant. For more information, see \sref{sec:errors:new}.
\docswitch{\ocoq} This switch causes \menhir to produce Coq code. See \sref{sec:coq}.
\docswitch{\ocoqlibpath \nt{path}} This switch allows specifying under what name (or path) the Coq support library
MenhirLib is known to Coq. When \menhir runs in \ocoq mode, the generated
parser contains references to several modules in this library. This path is
used to qualify these references. Its default value is \texttt{MenhirLib}.
\docswitch{\ocoqlibpath \nt{path}} This switch allows specifying under what
name (or path) the Coq support library is known to Coq. When \menhir runs in
\ocoq mode, the generated parser contains references to several modules in
this library. This path is used to qualify these references. Its default value
is \coqmenhirlib.
\docswitch{\ocoqlibnopath} This switch indicates that references to the Coq library MenhirLib
should \emph{not} be qualified. This was the default behavior of \menhir prior to 2018/05/30.
This switch is provided for compatibility, but normally should not be used.
\docswitch{\ocoqlibnopath} This switch indicates that references to the Coq
library \coqmenhirlib should \emph{not} be qualified. This was the default
behavior of \menhir prior to 2018/05/30. This switch is provided for
compatibility, but normally should not be used.
\docswitch{\ocoqnoactions} (Used in conjunction with \ocoq.) This switch
causes the semantic actions present in the \vy file to be ignored and
......@@ -154,6 +156,10 @@ sense of \sref{sec:conflicts:benign}). This can be desirable also because, for
a complex grammar, completeness may require a heavy certificate and its
validation by Coq may take time.
\docswitch{\ocoqnoversioncheck} (Used in conjunction with \ocoq.) This switch
prevents the generation of the check that verifies that the versions of
\menhir and \coqmenhirlib match.
\docswitch{\odepend} See \sref{sec:build}.
\docswitch{\odump} This switch causes a description of the automaton to be
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment