aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Lineartyping.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Lineartyping.v')
-rw-r--r--backend/Lineartyping.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 1fe23a9d..18594be8 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -321,6 +321,7 @@ Local Opaque mreg_type.
+ (* other ops *)
destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
econstructor; eauto.
+
apply wt_setreg; auto; try (apply wt_undef_regs; auto).
eapply Val.has_subtype; eauto.
change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.