From d18d82c9e58567384ea632c77a5c1531f6d534cb Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 20 Oct 1999 20:41:08 +0000
Subject:  - documentation repertoire proofs/  - IsAppL of constr * constr list
 ==> répercussion  - module Clenv (suite; as terminé)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@113 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/doc.tex | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 proofs/doc.tex

(limited to 'proofs/doc.tex')

diff --git a/proofs/doc.tex b/proofs/doc.tex
new file mode 100644
index 000000000..431027ef0
--- /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}
+
-- 
cgit v1.2.3