Commit 9b2972e7 authored by BECKER Benedikt's avatar BECKER Benedikt

Change default prefix of why3pp to WHY

parent e355611e
......@@ -1159,7 +1159,7 @@ print \whyml inductive definitions to \LaTeX{} (using the
(\texttt{-{}-kind=inductive}) when using the \LaTeX-output
(\texttt{-{}-output=latex}).
\item[\texttt{-{}-prefix=\textsl{<prefix>}}] Set the prefix for \LaTeX{}
commands to \texttt{\textsl{<prefix>}}. The default is \texttt{IND}.
commands to \texttt{\textsl{<prefix>}}. The default is \texttt{WHY}.
\item[\texttt{\textsl{<file>}[.\textsl{<Module>}].\textsl{<ind\_type>}}] One or
more inductive definitions for \texttt{-{}-output=latex} and
\texttt{-{}-kind=inductive}.
......
......@@ -412,7 +412,7 @@ let set_output = function
| "ast" -> output := Some Ast
| str -> ksprintf invalid_arg "output: --%s--" str
let prefix = ref "IND"
let prefix = ref "WHY"
let usage =
"Pretty print Why3 declarations (currently only inductive types in LaTeX using mathpartir).\n\
......@@ -421,7 +421,7 @@ let usage =
let options = [
"--output", Arg.String set_output, "<output> Output format";
"--kind", Arg.String set_kind, "<category> Syntactic category to be printed (--kind=inductive only possible value for --output=latex)";
"--prefix", Arg.String ((:=) prefix), "<prefix> Prefix for LaTeX commands (default for output latex: IND)";
"--prefix", Arg.String ((:=) prefix), "<prefix> Prefix for LaTeX commands (default for output latex: WHY)";
"-", Arg.Unit (fun () -> filename := Some "-"), " Read from stdin";
]
......
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