diff options
| -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} |