diff options
Diffstat (limited to 'proofs/doc.tex')
| -rw-r--r-- | proofs/doc.tex | 14 |
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} + |