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/Stackingproof.v') 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 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/Stackingproof.v') 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