En-tete doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3868 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 0 deletions

diff --git a/interp/doc.tex b/interp/doc.tex
new file mode 100644
index 000000000..4d60ec34f
--- /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}