diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | doc/intro.tex | 2 | ||||
| -rw-r--r-- | doc/macros.tex | 3 | ||||
| -rw-r--r-- | kernel/doc.tex | 6 | ||||
| -rw-r--r-- | lib/doc.tex | 4 |
5 files changed, 17 insertions, 3 deletions
@@ -36,8 +36,9 @@ OBJS=$(CONFIG) $(LIB) $(KERNEL) world: $(OBJS) -MLI=$(OBJS:.cmo=.mli) -LPFILES=doc/macros.tex $(MLI) +LPLIB = lib/doc.tex $(LIB:.cmo=.mli) +LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) +LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) lp: doc/coq.ps doc/coq.ps: doc/coq.tex cd doc; make coq.ps diff --git a/doc/intro.tex b/doc/intro.tex new file mode 100644 index 0000000000..a598ba6e77 --- /dev/null +++ b/doc/intro.tex @@ -0,0 +1,2 @@ + +\ocwsection This is \Coq, a proof assistant for the \CCI.
\ No newline at end of file diff --git a/doc/macros.tex b/doc/macros.tex index cbaa8e0375..5a4a2e74d4 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,4 +1,5 @@ % macros for coq.tex - +\newcommand{\Coq}{\textsf{Coq}} +\newcommand{\CCI}{Calculus of Inductive Constructions} diff --git a/kernel/doc.tex b/kernel/doc.tex new file mode 100644 index 0000000000..2d80109b7c --- /dev/null +++ b/kernel/doc.tex @@ -0,0 +1,6 @@ + +\section*{The Coq kernel} + +This section describes the \Coq\ kernel, which is a type checker for the \CCI. + +The modules of the kernel are organized as follows. diff --git a/lib/doc.tex b/lib/doc.tex new file mode 100644 index 0000000000..224da620a7 --- /dev/null +++ b/lib/doc.tex @@ -0,0 +1,4 @@ + +\section*{Utility libraries} + + |