diff options
Diffstat (limited to 'theories/NArith/BinNat.v')
| -rw-r--r-- | theories/NArith/BinNat.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 5b1e83e6c..61a77bf0e 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -893,11 +893,9 @@ Qed. (** Instantiation of generic properties of natural numbers *) -(** The Bind Scope prevents N to stay associated with abstract_scope. - (TODO FIX) *) - -Include NProp. Bind Scope N_scope with N. -Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Include NProp + <+ UsualMinMaxLogicalProperties + <+ UsualMinMaxDecProperties. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract @@ -983,6 +981,8 @@ Qed. End N. +Bind Scope N_scope with N.t N. + (** Exportation of notations *) Infix "+" := N.add : N_scope. |