From 2fd44905ab9eb1991dee9bcc0f3e4720135ab143 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 10 Oct 2003 19:06:03 +0000 Subject: Delimiters N devient 'nat' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4579 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Init/Datatypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Init/Datatypes.v') 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 ]. -- cgit v1.2.3