Commit 46784172 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Fix some documentation typos.

parent f4c52b97
...@@ -5,7 +5,8 @@ version 0.80, Oct 30, 2012 ...@@ -5,7 +5,8 @@ version 0.80, Oct 30, 2012
o new warning: form exists x, P -> Q o new warning: form exists x, P -> Q
o [replayer] new option -q o [replayer] new option -q
o [Provers] support for Coq 8.4 o [Provers] support for Coq 8.4
o New scheme for Coq realizations, using type classes o new scheme for Coq realizations, using type classes
* theory realizations now use meta "realized_theory" instead of "realized"
version 0.73, Jul 19, 2012 version 0.73, Jul 19, 2012
========================== ==========================
......
...@@ -100,7 +100,7 @@ let goal_id1 : Decl.prsymbol = ...@@ -100,7 +100,7 @@ let goal_id1 : Decl.prsymbol =
let task1 : Task.task = let task1 : Task.task =
Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1 Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
\end{ocamlcode} \end{ocamlcode}
To make the formula a goal, we must give a name to it, here "goal1". A To make the formula a goal, we must give a name to it, here ``goal1''. A
goal name has type \texttt{prsymbol}, for identifiers denoting goal name has type \texttt{prsymbol}, for identifiers denoting
propositions in a theory or a task. Notice again that the concrete propositions in a theory or a task. Notice again that the concrete
syntax of \why requires these symbols to be capitalized, but it is not syntax of \why requires these symbols to be capitalized, but it is not
......
...@@ -45,7 +45,7 @@ corresponding theory section of the driver. ...@@ -45,7 +45,7 @@ corresponding theory section of the driver.
\begin{verbatim} \begin{verbatim}
theory env_path.theory_name theory env_path.theory_name
meta "realized" "env_path.theory_name", "optional_naming" meta "realized_theory" "env_path.theory_name", "optional_naming"
end end
\end{verbatim} \end{verbatim}
...@@ -53,7 +53,7 @@ The first parameter is the theory name for \why. The second ...@@ -53,7 +53,7 @@ The first parameter is the theory name for \why. The second
parameter, if not empty, provides a name to be used inside generated parameter, if not empty, provides a name to be used inside generated
scripts to point to the realization, in case the default name is not scripts to point to the realization, in case the default name is not
suitable for the interactive prover. suitable for the interactive prover.
\index{realized@\verb+realized+} \index{realized_theory@\verb+realized_theory+}
\section{Generated/edited files} \section{Generated/edited files}
...@@ -107,7 +107,7 @@ use, it does not scale well when the realizations are to be shipped to ...@@ -107,7 +107,7 @@ use, it does not scale well when the realizations are to be shipped to
other users. Instead, one should create two additional files: a other users. Instead, one should create two additional files: a
configuration file that indicates how to modify paths, provers, and configuration file that indicates how to modify paths, provers, and
editors, and a driver file that contains only the needed editors, and a driver file that contains only the needed
\verb+meta "realized"+ declarations. The configuration file should be as \verb+meta "realized_theory"+ declarations. The configuration file should be as
follows. follows.
\index{configuration file} \index{configuration file}
......
...@@ -170,7 +170,7 @@ attempts and transformations were saved in a database --- an XML file ...@@ -170,7 +170,7 @@ attempts and transformations were saved in a database --- an XML file
created when the \why file was opened in the GUI for the first created when the \why file was opened in the GUI for the first
time. Then, for all the goals that remain unchanged, the previous time. Then, for all the goals that remain unchanged, the previous
proofs are shown again. For the parts that changed, the previous proofs are shown again. For the parts that changed, the previous
proofs attempts are shown but marked with "(obsolete)"\index{obsolete!proof attempt} proofs attempts are shown but marked with ``(obsolete)''\index{obsolete!proof attempt}
so that you so that you
know the results are not accurate. You can now retry to prove all what know the results are not accurate. You can now retry to prove all what
remains unproved using any of the provers. remains unproved using any of the provers.
......
Supports Markdown
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