From 53233447db377e5e0ee38cf880a4a3e88d2ccb58 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 Apr 2020 13:26:10 +0200
Subject: [PATCH] =?UTF-8?q?Support=20telescopic=20`=E2=88=80..`=20in=20`iS?=
 =?UTF-8?q?tartProof`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/coq_tactics.v  | 5 ++++-
 theories/proofmode/ltac_tactics.v | 2 ++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index d9613c1fe..daea5a760 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export bi.
+From iris.bi Require Export bi telescopes.
 From iris.bi Require Import tactics.
 From iris.proofmode Require Export base environments classes modality_instances.
 Set Default Proof Using "Type".
@@ -504,6 +504,9 @@ Proof. rewrite /IntoEmpValid => Hφ Hi1 Hi2. apply Hi1, Hi2, Hφ. Defined.
 Lemma into_emp_valid_forall {A} (φ : A → Type) P x :
   IntoEmpValid (φ x) P → IntoEmpValid (∀ x : A, φ x) P.
 Proof. rewrite /IntoEmpValid => Hi1 Hi2. apply Hi1, Hi2. Defined.
+Lemma into_emp_valid_tforall {TT : tele} (φ : TT → Prop) P x :
+  IntoEmpValid (φ x) P → IntoEmpValid (∀.. x : TT, φ x) P.
+Proof. rewrite /IntoEmpValid tforall_forall=> Hi1 Hi2. apply Hi1, Hi2. Defined.
 Lemma into_emp_valid_proj φ P : IntoEmpValid φ P → φ → ⊢ P.
 Proof. intros HP. apply HP. Defined.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 30bbab30d..7a5976c5b 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -785,6 +785,8 @@ Ltac iIntoEmpValid_go := first
      [(*goal for [φ] *)|iIntoEmpValid_go]
   |(* Case [∀ x : A, φ] *)
    notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid_go
+  |(* Case [∀.. x : TT, φ] *)
+   notypeclasses refine (into_emp_valid_tforall _ _ _ _); iIntoEmpValid_go
   |(* Case [P ⊢ Q], [P ⊣⊢ Q], [⊢ P] *)
    notypeclasses refine (into_emp_valid_here _ _ _)].
 
-- 
GitLab