diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:58:47 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-24 09:58:47 +0100 |
| commit | 66de649c75bc5625f0eab42d299f2281a3872510 (patch) | |
| tree | 8b5ee0df050bf06ea88a2ae382025d0ac9b0c8d6 /mppa_k1c | |
| parent | 82be9309276a2de2cff6ab96ef7f7b74bb34ffbb (diff) | |
| download | compcert-kvx-66de649c75bc5625f0eab42d299f2281a3872510.tar.gz compcert-kvx-66de649c75bc5625f0eab42d299f2281a3872510.zip | |
fixed typing issues
Diffstat (limited to 'mppa_k1c')
| -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. |