diff options
Diffstat (limited to 'theories/Numbers/Integer/SpecViaZ')
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index c339154499..788ca8e560 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -109,7 +109,7 @@ Module Type ZType. Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y]. Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y]. Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y]. - Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x]. + Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x]. End ZType. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index f8fa842836..8c1e7b4fa1 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -471,7 +471,7 @@ Qed. Lemma div2_spec : forall a, div2 a == shiftr a 1. Proof. - intros a. zify. now apply Zdiv2'_spec. + intros a. zify. now apply Zdiv2_spec. Qed. End ZTypeIsZAxioms. |