diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index eeec9042f..6948d420a 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1153,11 +1153,9 @@ Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. -(** The Bind Scope prevents Z to stay associated with abstract_scope. - (TODO FIX) *) - -Include ZProp. Bind Scope Z_scope with Z. -Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. +Include ZProp + <+ UsualMinMaxLogicalProperties + <+ UsualMinMaxDecProperties. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract @@ -1277,6 +1275,8 @@ Qed. End Z. +Bind Scope Z_scope with Z.t Z. + (** Re-export Notations *) Infix "+" := Z.add : Z_scope. |