Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 0 insertions, 14 deletions

diff --git a/proofs/doc.tex b/proofs/doc.tex
deleted file mode 100644
index 431027ef..00000000
--- a/proofs/doc.tex
+++ /dev/null
@@ -1,14 +0,0 @@
-
-\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}
-