diff options
Diffstat (limited to 'theories/Numbers/Natural/Peano/NPeano.v')
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 4578851e27..0cf9ae4416 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -756,9 +756,8 @@ Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _. (** Generic Properties *) -Include NProp [scope abstract_scope to nat_scope] - <+ UsualMinMaxLogicalProperties [scope abstract_scope to nat_scope] - <+ UsualMinMaxDecProperties [scope abstract_scope to nat_scope]. +Include NProp + <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. End Nat. |