From 08d096c5ee36af4c89c5d52ca045f00b8470402b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Nov 2017 17:23:36 +0100
Subject: [PATCH] Name more variables.

---
 theories/program_logic/language.v | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 365b9f221..b9d10beb8 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -145,12 +145,11 @@ Section language.
     PureExec φ (K e1) (K e2).
   Proof.
     intros [Hred Hstep]. split.
-    - intros σ ?. destruct (Hred σ) as (? & ? & ? & ?); first done.
-      do 3 eexists. eapply fill_step. done.
-    - intros σ ???? Hpstep. edestruct fill_step_inv as (? & ? & ?); [|exact Hpstep|].
-      + destruct (Hred σ) as (? & ? & ? & ?); first done.
-        eapply val_stuck. done.
-      + edestruct Hstep as (? & ? & ?); [done..|]. by subst.
+    - unfold reducible in *. naive_solver eauto using fill_step.
+    - intros σ1 e2' σ2 efs ? Hpstep.
+      destruct (fill_step_inv e1 σ1 e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
+      + destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
+      + edestruct (Hstep σ1 e2'' σ2 efs) as (-> & -> & ->); auto.
   Qed.
 
   (* This is a family of frequent assumptions for PureExec *)
-- 
GitLab