From dd4767e17235adb5de922626ed1fea15f4eb9e3b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 6 Apr 2021 23:37:22 +0200 Subject: Important commit on expansions' mini CSE, and a draft for addptrofs --- backend/Stackingproof.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backend') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d3fcdb91..08061aa4 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -868,7 +868,8 @@ Qed. Remark transl_destroyed_by_op: forall op e, destroyed_by_op (transl_op e op) = destroyed_by_op op. Proof. - intros; destruct op; reflexivity. + intros; destruct op; try reflexivity; simpl. + all: destruct optR as [[]|]; simpl; try reflexivity. Qed. Remark transl_destroyed_by_load: -- cgit