From ce46d445dba5a4363a3dd01274f77198c94ab0ef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 May 2017 10:59:17 +0200
Subject: [PATCH] Fix use of iInduction, we had to generalize first.

TODO: fix Iris to generate better error messages.
---
 theories/typing/function.v | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/theories/typing/function.v b/theories/typing/function.v
index b10f2d91..0b40d59f 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -275,14 +275,11 @@ Section typing.
       iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
       { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
       iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
-      + iApply "HE'". iFrame "#". iClear "Hf Hinh HE' LFT HE". clear.
-        (* FIXME: iInduction κs as [|κ κs] "IH". fails. *)
-        iRevert "Hκs". rewrite /coq_tactics.of_envs /=.
-        rewrite uPred.sep_elim_r. induction κs; iIntros "_ #Hκs"; simpl; first done.
+      + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
+        iInduction κs as [|κ κs] "IH" forall "Hκs"=> //=.
         iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
-        iApply IHκs; first by auto. iAlways.
-        iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
+        iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
         iFrame "#∗".
       + iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.
-- 
GitLab