From f0582c61ea565ce96227fbd44d83e6741eaa60f2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Mar 2017 20:55:09 +0100
Subject: [PATCH] Support strong framing of the whole spatial context.

---
 theories/proofmode/sel_patterns.v |  5 +++--
 theories/proofmode/tactics.v      | 10 +++++-----
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 99b4beb6b..7888dc301 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -5,7 +5,7 @@ Set Default Proof Using "Type".
 Inductive sel_pat :=
   | SelPure
   | SelPersistent
-  | SelSpatial
+  | SelSpatial : bool → sel_pat
   | SelName : bool → string → sel_pat.
 
 Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
@@ -23,7 +23,8 @@ Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :
   | TName s :: ts => parse_go ts (SelName false s :: k)
   | TPure :: ts => parse_go ts (SelPure :: k)
   | TAlways :: ts => parse_go ts (SelPersistent :: k)
-  | TSep :: ts => parse_go ts (SelSpatial :: k)
+  | THat :: TSep :: ts => parse_go ts (SelSpatial true :: k)
+  | TSep :: ts => parse_go ts (SelSpatial false :: k)
   | _ => None
   end.
 Definition parse (s : string) : option (list sel_pat) :=
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index f48957c36..b59d72dcd 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -76,7 +76,7 @@ Ltac iElaborateSelPat pat tac :=
        let Hs' := eval env_cbv in (env_dom (env_persistent Δ)) in
        let Δ' := eval env_cbv in (envs_clear_persistent Δ) in
        go pat Δ' ((ESelName true <$> Hs') ++ Hs)
-    | SelSpatial :: ?pat =>
+    | SelSpatial _ :: ?pat =>
        let Hs' := eval env_cbv in (env_dom (env_spatial Δ)) in
        let Δ' := eval env_cbv in (envs_clear_spatial Δ) in
        go pat Δ' ((ESelName false <$> Hs') ++ Hs)
@@ -202,15 +202,15 @@ Local Ltac iFrameAnyPersistent :=
      let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
   end.
 
-Local Ltac iFrameAnySpatial :=
+Local Ltac iFrameAnySpatial strong :=
   let rec go Hs :=
-    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp true H; go Hs end in
+    match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp strong H; go Hs end in
   match goal with
   | |- of_envs ?Δ ⊢ _ =>
      let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
   end.
 
-Tactic Notation "iFrame" := iFrameAnySpatial.
+Tactic Notation "iFrame" := iFrameAnySpatial false.
 
 Tactic Notation "iFrame" "(" constr(t1) ")" :=
   iFramePure t1.
@@ -239,7 +239,7 @@ Tactic Notation "iFrame" constr(Hs) :=
     | [] => idtac
     | SelPure :: ?Hs => iFrameAnyPure; go Hs
     | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
-    | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
+    | SelSpatial ?b :: ?Hs => iFrameAnySpatial b; go Hs
     | SelName ?b ?H :: ?Hs => iFrameHyp b H; go Hs
     end
   in let Hs := sel_pat.parse Hs in go Hs.
-- 
GitLab