diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-07 18:49:37 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:19 +0100 |
| commit | 55fe005b2141a69ffd9589568f8b854075174d56 (patch) | |
| tree | ff1a562959d4bb6bb44d751a4ee39cc791045d9f | |
| parent | 6d5a8e69517276d1d13275533aee9fceb42b9d13 (diff) | |
COMMENT: question
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 736affe94..29e4f256b 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1858,6 +1858,7 @@ reflexivity. \begin{coq_eval} Abort. \end{coq_eval} +% QUESTION: What are we trying to say with the above examples? % La disparition de Program devrait rendre la construction Match obsolete % \subsubsection{The {\tt Match \ldots with \ldots end} expression} |