diff options
Diffstat (limited to 'theories/Numbers/Natural/Peano/NPeano.v')
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index a510b3ae2..5e36916b9 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -800,6 +800,8 @@ Include NProp End Nat. +Bind Scope nat_scope with Nat.t nat. + (** [Nat] contains an [order] tactic for natural numbers *) (** Note that [Nat.order] is domain-agnostic: it will not prove |