Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 14 insertions, 0 deletions

diff --git a/interp/doc.tex b/interp/doc.tex
new file mode 100644
index 00000000..4d60ec34
--- /dev/null
+++ b/interp/doc.tex
@@ -0,0 +1,14 @@
+
+\newpage
+\section*{The interpretation of Coq front abstract syntax of terms}
+
+\ocwsection \label{library}
+This chapter describes the translation from \Coq\ context-dependent
+front abstract syntax of terms (\verb=front=} to and from the
+context-free, untyped, raw form of constructions (\verb=rawconstr=).
+
+The modules translating back and forth the front abstract syntax are
+organized as follows.
+
+\bigskip
+\begin{center}\epsfig{file=library.dep.ps}\end{center}