diff options
| author | Matěj Grabovský | 2015-03-27 16:08:29 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-03-31 11:27:59 +0200 |
| commit | 829238f2fe74c782023989e1871e15411b3e4ada (patch) | |
| tree | 5b3cee1bfe1b5aefbe7304caf20e08f12116e534 /doc/refman/Program.tex | |
| parent | bc480550dbd705384bec15968dbdde0987df311c (diff) | |
Fix various typos in documentation
Closes #57.
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index e802398b55..76bcaaae67 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -5,7 +5,7 @@ We present here the \Program\ tactic commands, used to build certified \Coq\ programs, elaborating them from their algorithmic skeleton and a -rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction +rich specification \cite{Sozeau06}. It can be thought of as a dual of extraction (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole \Coq{} proof @@ -48,7 +48,7 @@ operation (see Section~\ref{Caseexpr}). | S n => u end. \end{coq_example*} -will be first rewrote to: +will be first rewritten to: \begin{coq_example*} (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t @@ -108,7 +108,7 @@ goals to construct the final definitions. \subsection{\tt Program Definition {\ident} := {\term}. \comindex{Program Definition}\label{ProgramDefinition}} -This command types the value {\term} in \Russell\ and generate proof +This command types the value {\term} in \Russell\ and generates proof obligations. Once solved using the commands shown below, it binds the final \Coq\ term to the name {\ident} in the environment. |