diff options
| author | Pierre Letouzey | 2015-04-09 14:46:37 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2015-04-09 14:46:37 +0200 |
| commit | 429f493997e34bfaac930c68bf6b267a5b9640ee (patch) | |
| tree | 28f15d0aeff2ce899a312f31e10fe2030b2dd813 /doc/refman/Program.tex | |
| parent | aeec29a177e8f1c89996c0449e4cd81ca3ca4377 (diff) | |
| parent | eaa3f9719d6190ba92ce55816f11c70b30434309 (diff) | |
Merge branch 'v8.5' into trunk
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. |