From e37d655db0ec3d2c002e200c3e70a1997e39a458 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Apr 2021 17:13:23 +0200 Subject: removing unusued proof line --- backend/Stackingproof.v | 1 - 1 file changed, 1 deletion(-) (limited to 'backend') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 08061aa4..a5aa5177 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -869,7 +869,6 @@ Remark transl_destroyed_by_op: forall op e, destroyed_by_op (transl_op e op) = destroyed_by_op op. Proof. intros; destruct op; try reflexivity; simpl. - all: destruct optR as [[]|]; simpl; try reflexivity. Qed. Remark transl_destroyed_by_load: -- cgit