From 829238f2fe74c782023989e1871e15411b3e4ada Mon Sep 17 00:00:00 2001
From: Matěj Grabovský
Date: Fri, 27 Mar 2015 16:08:29 +0100
Subject: Fix various typos in documentation

Closes #57.
---
 doc/refman/Program.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/refman/Program.tex')

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.
 
-- 
cgit v1.2.3