aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--backend/Stackingproof.v1
1 files changed, 0 insertions, 1 deletions
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: