diff options
| -rw-r--r-- | mppa_k1c/Conventions1.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Conventions1.v b/mppa_k1c/Conventions1.v index ac2117d0..48346a6d 100644 --- a/mppa_k1c/Conventions1.v +++ b/mppa_k1c/Conventions1.v @@ -130,7 +130,7 @@ Lemma loc_result_pair: match loc_result sg with | One _ => True | Twolong r1 r2 => - r1 <> r2 /\ sg.(sig_res) = Tlong + r1 <> r2 /\ proj_sig_res sg = Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.ptr64 = false end. |