From 917859721f6423b24788ec6219774b5196b02ec1 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Thu, 1 Mar 2018 14:45:06 +0100
Subject: MPPA - Machregs + Conventions1 + backend proof tweaking

---
 backend/Lineartyping.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/Lineartyping.v')

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 30cc0d91..d5fadd4c 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -291,7 +291,7 @@ Local Opaque mreg_type.
     apply wt_setreg; auto. eapply Val.has_subtype; eauto.
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
-    destruct args; try discriminate. destruct args; discriminate.
+    destruct args; try discriminate. destruct args; discriminate;
     apply wt_undef_regs; auto.
 - (* load *)
   simpl in *; InvBooleans.
-- 
cgit