From 911412f9138ac659062d011339426815d6bf2ee9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 25 May 2019 21:08:06 +0200
Subject: [PATCH] Port `tac_assumption`.

---
 theories/proofmode/coq_tactics.v  | 14 +++++++-------
 theories/proofmode/ltac_tactics.v |  6 +++---
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 4777cb8af..ae011cf5b 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -61,17 +61,17 @@ Proof. intros H. induction H; simpl; apply _. Qed.
 Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
 Proof. intros. by rewrite envs_entails_eq (affine (of_envs Δ)). Qed.
 
-(* TODO: convert to not take Δ' *)
-Lemma tac_assumption Δ Δ' i p P Q :
-  envs_lookup_delete true i Δ = Some (p,P,Δ') →
+Lemma tac_assumption Δ i p P Q :
+  envs_lookup i Δ = Some (p,P) →
   FromAssumption p P Q →
-  (if env_spatial_is_nil Δ' then TCTrue
+  (let Δ' := envs_delete true i p Δ in
+   if env_spatial_is_nil Δ' then TCTrue
    else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
   envs_entails Δ Q.
 Proof.
-  intros ?? H. rewrite envs_entails_eq envs_lookup_delete_sound //.
-  destruct (env_spatial_is_nil Δ') eqn:?.
-  - by rewrite (env_spatial_is_nil_intuitionistically Δ') // sep_elim_l.
+  intros ?? H. rewrite envs_entails_eq envs_lookup_sound //.
+  simpl in *. destruct (env_spatial_is_nil _) eqn:?.
+  - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
 Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 4b47f0e25..dc975db74 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -228,7 +228,7 @@ Ltac, but it may be possible in Ltac2. *)
 
 (** * Assumptions *)
 Tactic Notation "iExact" constr(H) :=
-  eapply tac_assumption with _ H _ _; (* (i:=H) *)
+  eapply tac_assumption with H _ _; (* (i:=H) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
      fail "iExact:" H "not found"
@@ -262,7 +262,7 @@ Tactic Notation "iAssumption" :=
     lazymatch Γ with
     | Esnoc ?Γ ?j ?P => first
        [pose proof (_ : FromAssumption p P Q) as Hass;
-        eapply (tac_assumption _ _ j p P);
+        eapply (tac_assumption _ j p P);
           [pm_reflexivity
           |apply Hass
           |pm_reduce; iSolveTC ||
@@ -1051,7 +1051,7 @@ premises [n], the tactic will have the following behavior:
 actual error. *)
 Local Ltac iApplyHypExact H :=
   first
-    [eapply tac_assumption with _ H _ _; (* (i:=H) *)
+    [eapply tac_assumption with H _ _; (* (i:=H) *)
        [pm_reflexivity || fail 1
        |iSolveTC || fail 1
        |pm_reduce; iSolveTC]
-- 
GitLab