Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 14 insertions, 0 deletions

diff --git a/proofs/doc.tex b/proofs/doc.tex
new file mode 100644
index 00000000..431027ef
--- /dev/null
+++ b/proofs/doc.tex
@@ -0,0 +1,14 @@
+
+\newpage
+\section*{The Proof Engine}
+
+\ocwsection \label{proofs}
+This chapter describes the \Coq\ proof engine, which is also called
+the ``refiner'', since it provides a way to build terms by successive
+refining steps. Those steps are either primitive rules or higher-level
+tactics.
+The modules of the proof engine are organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=proofs.dep.ps,width=\linewidth}\end{center}
+