From e1c864b670812eda55e0ee129855c69d32c8b84a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 3 May 2019 10:34:58 +0200
Subject: it compiles

---
 mppa_k1c/Peephole.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mppa_k1c/Peephole.v')

diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v
index 2c73bb63..91936ac6 100644
--- a/mppa_k1c/Peephole.v
+++ b/mppa_k1c/Peephole.v
@@ -34,8 +34,8 @@ Fixpoint optimize_body (insns : list basic) : list basic :=
     match t0 with
     | h1 :: t1 =>
         match h0, h1 with
-        | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)),
-          (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) =>
+        | (PStoreRRO Psd_a rs0 ra0 ofs0),
+          (PStoreRRO Psd_a rs1 ra1 ofs1) =>
           match gpreg_q_search rs0 rs1 with
           | Some rs0rs1 =>
             let zofs0 := Ptrofs.signed ofs0 in
-- 
cgit