Commit 412b6e68 authored by MARCHE Claude's avatar MARCHE Claude

doc: specific Coq features

parent df417ca3
......@@ -52,6 +52,12 @@ It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
If you want to use the specific Coq features, i.e the Coq
tactic~\ref{chap:tactic} and Coq realizations~\ref{chap:realizations},
then Coq has to be installed before \why. Look at the summary printed
at the end of the configuration script to check if Coq has been
detected properly.
When configuration is finished, you can compile \why.
\begin{verbatim}
make
......
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