From 977f570ceced645c3b4a5cd7226f61917a0c1ad4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 20 Dec 2016 23:07:07 +0100
Subject: [PATCH] Robbert fixed intro patterns in proofmode :)

---
 opam.pins                  | 2 +-
 theories/typing/cont.v     | 5 ++---
 theories/typing/function.v | 5 ++---
 3 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/opam.pins b/opam.pins
index 9d848526..cf8bb509 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq adfa07525e071b2a47aed37dac276aa38c10099d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9c55bc2cb196512e08ad8756722ac127e539a1da
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 5ceeda53..9d529dab 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -12,7 +12,7 @@ Section cont_typing.
     tctx_incl E L T (T' args) →
     typed_body E L [CCtx_iscont k L n T'] T (k (of_val <$> (args : list _))).
   Proof.
-    iIntros (Hincl). iIntros (tid qE) "#LFT HE HL HC HT".
+    iIntros (Hincl tid qE) "#LFT HE HL HC HT".
     iMod (Hincl with "LFT HE HL HT") as "(HE & HL & HT)".
     iSpecialize ("HC" with "HE * []"); first by (iPureIntro; apply elem_of_list_singleton).
     simpl. iApply ("HC" with "* HL HT").
@@ -25,8 +25,7 @@ Section cont_typing.
     (∀ k, typed_body E (L1 ++ L2) (CCtx_iscont k L1 n T' :: C) T (subst' kb k e2)) →
     typed_body E (L1 ++ L2) C T (let: kb := e1 in e2).
   Proof.
-    intros -> Hc1 Hc2 Hecont He2. iIntros (tid qE) "#LFT HE HL HC HT".
-    iApply wp_let'.
+    iIntros (-> Hc1 Hc2 Hecont He2 tid qE) "#LFT HE HL HC HT". iApply wp_let'.
     { simpl. rewrite decide_left. done. }
     iModIntro. iApply (He2 with "* LFT HE HL [HC] HT"). clear He2.
     iIntros "HE". iLöb as "IH". iIntros (x) "H".
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5b4f5dd1..ba5aea81 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -96,8 +96,7 @@ Section fn.
     typed_body E L [CCtx_iscont k L 1 (λ v, (TCtx_hasty (v!!!0) (ty x)) :: T')]
                (TCtx_hasty p (fn E' tys ty) :: T) (p (of_val k :: ps)).
   Proof.
-    (* FIXME: Why can't I merge these iIntros? *)
-    iIntros (HTsat HEsat). iIntros (tid qE) "#LFT HE HL HC".
+    iIntros (HTsat HEsat tid qE) "#LFT HE HL HC".
     rewrite tctx_interp_cons. iIntros "[Hf HT]".
     wp_bind p. iApply (wp_hasty with "Hf"). iIntros (v) "[% Hf]".
     iMod (HTsat with "LFT HE HL HT") as "(HE & HL & HT)". rewrite tctx_interp_app.
@@ -144,7 +143,7 @@ Section fn.
                  (subst' fb f $ subst_vec (kb ::: argsb) (Vector.map of_val $ k ::: args) e)) →
     typed_instruction_ty E L (zip_with TCtx_hasty cps ctyl) ef (fn E' tys ty).
   Proof.
-    iIntros (-> Hc Hbody). iIntros (tid qE) "!# #LFT $ $ #HT". iApply wp_value.
+    iIntros (-> Hc Hbody tid qE) "!# #LFT $ $ #HT". iApply wp_value.
     { simpl. rewrite decide_left. done. }
     rewrite tctx_interp_singleton. iLöb as "IH". iExists _. iSplit.
     { simpl. rewrite decide_left. done. }
-- 
GitLab