aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rwxr-xr-xtheories/Init/Datatypes.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 65d0722c3c..2d35928c54 100755
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -30,7 +30,7 @@ Add Printing If bool.
Inductive nat : Set := O : nat
| S : nat->nat.
-Delimits Scope nat_scope with N.
+Delimits Scope nat_scope with nat.
Bind Scope nat_scope with nat.
Arguments Scope S [ nat_scope ].