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 0000000000..4ce5811da3 --- /dev/null +++ b/interp/doc.tex @@ -0,0 +1,14 @@ + +\newpage +\section*{The interpretation of Coq front abstract syntax of terms} + +\ocwsection \label{interp} +This chapter describes the translation from \Coq\ context-dependent +front abstract syntax of terms (\verb=front=) to and from the +context-free, untyped, globalized form of constructions (\verb=glob_constr=). + +The modules translating back and forth the front abstract syntax are +organized as follows. + +\bigskip +\begin{center}\epsfig{file=interp.dep.ps}\end{center} |