diff options
Diffstat (limited to 'theories/Numbers/Natural/Binary/NBinary.v')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index cf284a2f19..bd59ef494b 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -234,9 +234,8 @@ Definition lor := Nor. Definition ldiff := Ndiff. Definition div2 := Ndiv2. -Include NProp [scope abstract_scope to N_scope] - <+ UsualMinMaxLogicalProperties [scope abstract_scope to N_scope] - <+ UsualMinMaxDecProperties [scope abstract_scope to N_scope]. +Include NProp + <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. End N. |