From 553714035fc08f9b145b89b3dd7c455f06e917df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Dec 2019 21:39:20 +0100 Subject: finish merge --- 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 994d2652..3fe61470 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -328,7 +328,7 @@ Local Opaque mreg_type. 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. - apply wt_undef_regs; auto. + (* no longer needed apply wt_undef_regs; auto. *) - (* load *) simpl in *; InvBooleans. econstructor; eauto. -- cgit