Commit 1ef5d144 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Document the issue with realization dependencies.

parent 87c816a8
......@@ -161,7 +161,7 @@ See manual Section xx
manpages.tex:809:\section{The \texttt{why3doc} tool} \todo{Documenter}
- (GUILLAUME) Realisations Coq, comment fait l'utilisateur pour faire
- DONE (GUILLAUME) Realisations Coq, comment fait l'utilisateur pour faire
ses realisations ne pas oublier de dire que les dependances avec le
.why ou .mlw: ne sera pas vérifié
......@@ -17,6 +17,11 @@ target directory already contains a file with the same name, \why
extracts all the parts that it assumes to be user-made and prints them in
the generated file.
Note that \why does not track dependencies between realizations and
theories, so a realization will become outdated if a theory is modified.
It is up to the user to handle such dependencies, for instance by adding
a Makefile rule.
\section{Using realizations inside proofs}
If a theory has been realized, a \why printer for an interactive prover
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