diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-08-20 15:12:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-08-20 15:12:41 +0000 |
| commit | cd9afd3c84949dff733ab59f3bf838bc5863b532 (patch) | |
| tree | 1fc1f25ea904c6fec7ab61bda63d20e5bbd66e28 | |
| parent | e08245e74ef52395052b926fc39d79e52f59af09 (diff) | |
programmation literaire : un fichier de description par repertoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@19 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 000000000..a598ba6e7 --- /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 cbaa8e037..5a4a2e74d 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 000000000..2d80109b7 --- /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 000000000..224da620a --- /dev/null +++ b/lib/doc.tex @@ -0,0 +1,4 @@ + +\section*{Utility libraries} + + |