diff options
Diffstat (limited to 'mppa_k1c/Asmblockgenproof1.v')
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index d90b73e2..99ab1b91 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1661,8 +1661,8 @@ Opaque Int.eq. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. simpl. - rewrite int64_eq_comm. - destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. |