From 5631ccb7c416bb7ecbe7920cb432a78436c0a7ac Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Mon, 26 Nov 2018 17:35:31 +0100
Subject: BROKEN - works for x86, not for k1 anymore

---
 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 55d86448..fc163719 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -324,7 +324,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