diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-19 17:48:34 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-19 17:48:34 +0000 |
commit | c1e8b8c5cbc0e19703b9b7326401e242cd751b80 (patch) | |
tree | 1d09fa39c291fa810158a5e46d44a000c96f5296 /doc/RefMan-gal.tex | |
parent | bef467cfac0b718bffdbb5444b2a4364b3941b09 (diff) |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8424 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-gal.tex')
-rw-r--r-- | doc/RefMan-gal.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index 73250efd3..c486be344 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -1201,10 +1201,10 @@ error message: \begin{coq_eval} Set Printing Depth 50. -\end{coq_eval} -\begin{coq_example} (********** The following is not correct and should produce **********) (********* Error: Recursive call to wrongplus ... **********) +\end{coq_eval} +\begin{coq_example} Fixpoint wrongplus (n m:nat) {struct n} : nat := match m with | O => n @@ -1317,10 +1317,10 @@ function does not satisfy the guard condition: \begin{coq_eval} Set Printing Depth 50. -\end{coq_eval} -\begin{coq_example*} (********** The following is not correct and should produce **********) (***************** Error: Unguarded recursive call *******************) +\end{coq_eval} +\begin{coq_example*} CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream := if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s). \end{coq_example*} |