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