From 66de649c75bc5625f0eab42d299f2281a3872510 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 24 Feb 2020 09:58:47 +0100 Subject: fixed typing issues --- mppa_k1c/Conventions1.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mppa_k1c') 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. -- cgit