diff options
Diffstat (limited to 'theories/Numbers/Integer/Binary')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index eab33051d4..8ed42ed8d9 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -202,7 +202,7 @@ Definition land_spec := Zand_spec. Definition lor_spec := Zor_spec. Definition ldiff_spec := Zdiff_spec. Definition lxor_spec := Zxor_spec. -Definition div2_spec := Zdiv2'_spec. +Definition div2_spec := Zdiv2_spec. Definition testbit := Ztestbit. Definition shiftl := Zshiftl. @@ -211,7 +211,7 @@ Definition land := Zand. Definition lor := Zor. Definition ldiff := Zdiff. Definition lxor := Zxor. -Definition div2 := Zdiv2'. +Definition div2 := Zdiv2. (** We define [eq] only here to avoid refering to this [eq] above. *) |