diff options
| -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... %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % |