diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-19 14:17:35 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-19 14:17:35 +0000 |
| commit | 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 (patch) | |
| tree | 5a5a73ee8770cba524b8c24892f709a308e9ab3b /kernel/doc.tex | |
| parent | 5393ee683be9e19ab25888925f561ea4f4b1dddb (diff) | |
- un effort sur la doc (ocamlweb)
- module Nametab
- module Impargs
- correction bug : Parameter id : t => vérification que t est bien un type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/doc.tex')
| -rw-r--r-- | kernel/doc.tex | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/doc.tex b/kernel/doc.tex index 56debc102..4a9fc3550 100644 --- a/kernel/doc.tex +++ b/kernel/doc.tex @@ -1,9 +1,11 @@ +\newpage \section*{The Coq kernel} \ocwsection \label{kernel} -This section describes the \Coq\ kernel, which is a type checker for the \CCI. - +This chapter describes the \Coq\ kernel, which is a type checker for the \CCI. The modules of the kernel are organized as follows. -TODO +\bigskip +\begin{center}\epsfig{file=kernel.dep.ps,width=\linewidth}\end{center} + |