diff options
| author | kirchner | 2004-03-12 13:52:04 +0000 |
|---|---|---|
| committer | kirchner | 2004-03-12 13:52:04 +0000 |
| commit | 212215f774d4945f5adaa2319488e5b8859daaf6 (patch) | |
| tree | 9f7402000c532f7c501235b4611868f68a10de2a | |
| parent | dfa0a72c50d5081b094b48f23fa905e5bbcf8062 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8491 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/newfaq/core.tex | 8 | ||||
| -rw-r--r-- | doc/newfaq/main.tex | 10 |
2 files changed, 15 insertions, 3 deletions
diff --git a/doc/newfaq/core.tex b/doc/newfaq/core.tex index 0ab238f59c..2e65ea7f19 100644 --- a/doc/newfaq/core.tex +++ b/doc/newfaq/core.tex @@ -1,2 +1,6 @@ -Gallina ? \\ -tactiques, tacticals, par cas (logique, entiers, constructeurs...) +\subsection{Predicate Calculus} + +\subsection{Induction} + +\subsection{Modules} + diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 023202a623..a49d1dcd2c 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -1,5 +1,6 @@ \documentclass[a4paper]{faq} +\pagestyle{plain} % yay les symboles \usepackage{stmaryrd} @@ -42,7 +43,14 @@ pointers to other references when possible. \newpage \section{Introduction} - +This FAQ is the sum of the questions that came to mind as we developed +proofs in \Coq. Since we are singularly short-minded, we wrote the +answers we found on bits of papers to have them at hand whenever the +situation occurs again. This, is the result of that: a collection of +tips one can refer to when proofs become intricate. Yes, this means we +won't take the blame for the shortcomings of the following. But if you +want to contribute and send in your own tricks, feel free to write to +us... %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % |