diff options
Diffstat (limited to 'doc/refman/Cases.tex')
| -rw-r--r-- | doc/refman/Cases.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 51ec2ef81..4238bf6a5 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -194,7 +194,7 @@ system. Here is an example: Set Printing Depth 50. \end{coq_eval} \begin{coq_example} -Check (fun x:nat => +Fail Check (fun x:nat => match x with | O => true | S _ => false @@ -271,7 +271,7 @@ When we use parameters in patterns there is an error message: Set Printing Depth 50. \end{coq_eval} \begin{coq_example} -Check +Fail Check (fun l:List nat => match l with | nil A => nil nat |