From 8760a7f81efda41753cf7592d6c3f974df2fd947 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 23 Nov 2003 20:15:10 +0000
Subject: Suppression %N

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8368 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/Coercion.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/doc/Coercion.tex b/doc/Coercion.tex
index 96fb492727..e29d10a90f 100644
--- a/doc/Coercion.tex
+++ b/doc/Coercion.tex
@@ -337,11 +337,11 @@ We first give an example of coercion between atomic inductive types
 
 %\begin{\small}
 \begin{coq_example}
-Definition bool_in_nat (b:bool) := if b then 0%N else 1%N.
+Definition bool_in_nat (b:bool) := if b then 0 else 1.
 Coercion bool_in_nat : bool >-> nat.
-Check (0%N = true).
+Check (0 = true).
 Set Printing Coercions.
-Check (0%N = true).
+Check (0 = true).
 \end{coq_example}
 %\end{small}
 
@@ -469,9 +469,9 @@ Parameter bij : Set -> Set -> Set.
 Parameter ap : forall A B:Set, bij A B -> A -> B.
 Coercion ap : bij >-> Funclass.
 Parameter b : bij nat nat.
-Check (b 0%N).
+Check (b 0).
 Set Printing Coercions.
-Check (b 0%N).
+Check (b 0).
 \end{coq_example}
 %\end{small}
 
-- 
cgit v1.2.3