From 75c165b21b67e07668ce33207bf993d33b35ac1b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 25 Dec 2018 10:13:57 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20persistent=20=E2=86=92=20intuitionisti?=
 =?UTF-8?q?c=20for=20proofmode=20internals/error=20messages.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/classes.v        |  2 +-
 theories/proofmode/coq_tactics.v    | 88 ++++++++++++++---------------
 theories/proofmode/environments.v   | 20 +++----
 theories/proofmode/intro_patterns.v | 18 +++---
 theories/proofmode/ltac_tactics.v   | 70 +++++++++++------------
 theories/proofmode/reduction.v      |  2 +-
 theories/proofmode/sel_patterns.v   |  4 +-
 theories/proofmode/spec_patterns.v  |  6 +-
 8 files changed, 105 insertions(+), 105 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index b49038240..310bcaabd 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -601,7 +601,7 @@ with the exception of:
 - [FromAssumption] used by [iAssumption]
 - [Frame] and [MaybeFrame] used by [iFrame]
 - [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
-- [IntoPersistent] used by [iPersistent]
+- [IntoPersistent] used by [iIntuitionistic]
 *)
 Instance into_pure_tc_opaque {PROP : bi} (P : PROP) φ :
   IntoPure P φ → IntoPure (tc_opaque P) φ := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 09cba8b02..2c6766fab 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -135,8 +135,8 @@ Qed.
 Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
 Proof. rewrite envs_entails_eq. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
-(** * Persistence *)
-Lemma tac_persistent Δ Δ' i p P P' Q :
+(** * Intuitionistic *)
+Lemma tac_intuitionistic Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
@@ -170,7 +170,7 @@ Proof.
   - apply impl_intro_l. rewrite envs_app_singleton_sound //; simpl.
     by rewrite -(from_affinely P') persistent_and_affinely_sep_l_1 wand_elim_r.
 Qed.
-Lemma tac_impl_intro_persistent Δ Δ' i P P' Q R :
+Lemma tac_impl_intro_intuitionistic Δ Δ' i P P' Q R :
   FromImpl R P Q →
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
@@ -195,7 +195,7 @@ Proof.
   rewrite /FromWand envs_entails_eq => <- ? HQ.
   rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
-Lemma tac_wand_intro_persistent Δ Δ' i P P' Q R :
+Lemma tac_wand_intro_intuitionistic Δ Δ' i P P' Q R :
   FromWand R P Q →
   IntoPersistent false P P' →
   TCOr (Affine P) (Absorbing Q) →
@@ -234,7 +234,7 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
 Proof.
   rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hj ? Hj' <-.
   rewrite (envs_lookup_sound' _ false) //; simpl. destruct p; simpl.
-  - move: Hj; rewrite envs_delete_persistent=> Hj.
+  - move: Hj; rewrite envs_delete_intuitionistic=> Hj.
     rewrite envs_simple_replace_singleton_sound //; simpl.
     rewrite -intuitionistically_if_idemp -intuitionistically_idemp into_wand /=.
     rewrite assoc (intuitionistically_intuitionistically_if q).
@@ -296,7 +296,7 @@ Proof.
   by rewrite emp_wand wand_elim_r.
 Qed.
 
-Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P1' P2 R Q :
+Lemma tac_specialize_assert_intuitionistic Δ Δ' Δ'' j q P1 P1' P2 R Q :
   envs_lookup_delete true j Δ = Some (q, R, Δ') →
   IntoWand q true R P1 P2 →
   Persistent P1 →
@@ -315,7 +315,7 @@ Proof.
   by rewrite intuitionistically_if_sep_2 into_wand wand_elim_l wand_elim_r.
 Qed.
 
-Lemma tac_specialize_persistent_helper Δ Δ'' j q P R R' Q :
+Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q :
   envs_lookup j Δ = Some (q,P) →
   envs_entails Δ (<absorb> R) →
   IntoPersistent false R R' →
@@ -333,7 +333,7 @@ Qed.
 
 (* A special version of [tac_assumption] that does not do any of the
 [FromAssumption] magic. *)
-Lemma tac_specialize_persistent_helper_done Δ i q P :
+Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
   envs_lookup i Δ = Some (q,P) →
   envs_entails Δ (<absorb> P).
 Proof.
@@ -631,8 +631,8 @@ End bi_tactics.
 (** The following _private_ classes are used internally by [tac_modal_intro] /
 [iModIntro] to transform the proofmode environments when introducing a modality.
 
-The class [TransformPersistentEnv M C Γin Γout] is used to transform the
-persistent environment using a type class [C].
+The class [TransformIntuitionisticEnv M C Γin Γout] is used to transform the
+intuitionistic environment using a type class [C].
 
 Inputs:
 - [Γin] : the original environment.
@@ -643,18 +643,18 @@ Inputs:
 
 Outputs:
 - [Γout] : the resulting environment. *)
-Class TransformPersistentEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
+Class TransformIntuitionisticEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
     (C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1) := {
-  transform_persistent_env :
+  transform_intuitionistic_env :
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
     (∀ P Q, M P ∧ M Q ⊢ M (P ∧ Q)) →
     □ ([∧] Γin) ⊢ M (□ ([∧] Γout));
-  transform_persistent_env_wf : env_wf Γin → env_wf Γout;
-  transform_persistent_env_dom i : Γin !! i = None → Γout !! i = None;
+  transform_intuitionistic_env_wf : env_wf Γin → env_wf Γout;
+  transform_intuitionistic_env_dom i : Γin !! i = None → Γout !! i = None;
 }.
 
-(* The class [TransformPersistentEnv M C Γin Γout filtered] is used to transform
-the persistent environment using a type class [C].
+(* The class [TransformIntuitionisticEnv M C Γin Γout filtered] is used to transform
+the intuitionistic environment using a type class [C].
 
 Inputs:
 - [Γin] : the original environment.
@@ -676,8 +676,8 @@ Class TransformSpatialEnv {PROP1 PROP2} (M : modality PROP1 PROP2)
   transform_spatial_env_dom i : Γin !! i = None → Γout !! i = None;
 }.
 
-(* The class [IntoModalPersistentEnv M Γin Γout s] is used to transform the
-persistent environment with respect to the behavior needed to introduce [M] as
+(* The class [IntoModalIntuitionisticEnv M Γin Γout s] is used to transform the
+intuitionistic environment with respect to the behavior needed to introduce [M] as
 given by [s : modality_intro_spec PROP1 PROP2].
 
 Inputs:
@@ -688,24 +688,24 @@ Inputs:
 
 Outputs:
 - [Γout] : the resulting environment. *)
-Inductive IntoModalPersistentEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
+Inductive IntoModalIntuitionisticEnv {PROP2} : ∀ {PROP1} (M : modality PROP1 PROP2)
     (Γin : env PROP2) (Γout : env PROP1), modality_action PROP1 PROP2 → Prop :=
-  | MIEnvIsEmpty_persistent {PROP1} (M : modality PROP1 PROP2) :
-     IntoModalPersistentEnv M Enil Enil MIEnvIsEmpty
-  | MIEnvForall_persistent (M : modality PROP2 PROP2) (C : PROP2 → Prop) Γ :
+  | MIEnvIsEmpty_intuitionistic {PROP1} (M : modality PROP1 PROP2) :
+     IntoModalIntuitionisticEnv M Enil Enil MIEnvIsEmpty
+  | MIEnvForall_intuitionistic (M : modality PROP2 PROP2) (C : PROP2 → Prop) Γ :
      TCForall C (env_to_list Γ) →
-     IntoModalPersistentEnv M Γ Γ (MIEnvForall C)
-  | MIEnvTransform_persistent {PROP1}
+     IntoModalIntuitionisticEnv M Γ Γ (MIEnvForall C)
+  | MIEnvTransform_intuitionistic {PROP1}
        (M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout :
-     TransformPersistentEnv M C Γin Γout →
-     IntoModalPersistentEnv M Γin Γout (MIEnvTransform C)
-  | MIEnvClear_persistent {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
-     IntoModalPersistentEnv M Γ Enil MIEnvClear
-  | MIEnvId_persistent (M : modality PROP2 PROP2) Γ :
-     IntoModalPersistentEnv M Γ Γ MIEnvId.
-Existing Class IntoModalPersistentEnv.
-Existing Instances MIEnvIsEmpty_persistent MIEnvForall_persistent
-  MIEnvTransform_persistent MIEnvClear_persistent MIEnvId_persistent.
+     TransformIntuitionisticEnv M C Γin Γout →
+     IntoModalIntuitionisticEnv M Γin Γout (MIEnvTransform C)
+  | MIEnvClear_intuitionistic {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
+     IntoModalIntuitionisticEnv M Γ Enil MIEnvClear
+  | MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
+     IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
+Existing Class IntoModalIntuitionisticEnv.
+Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
+  MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
 
 (* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
 environment with respect to the behavior needed to introduce [M] as given by
@@ -742,15 +742,15 @@ Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
 Section tac_modal_intro.
   Context {PROP1 PROP2 : bi} (M : modality PROP1 PROP2).
 
-  Global Instance transform_persistent_env_nil C : TransformPersistentEnv M C Enil Enil.
+  Global Instance transform_intuitionistic_env_nil C : TransformIntuitionisticEnv M C Enil Enil.
   Proof.
     split; [|eauto using Enil_wf|done]=> /= ??.
     rewrite !intuitionistically_True_emp -modality_emp //.
   Qed.
-  Global Instance transform_persistent_env_snoc (C : PROP2 → PROP1 → Prop) Γ Γ' i P Q :
+  Global Instance transform_intuitionistic_env_snoc (C : PROP2 → PROP1 → Prop) Γ Γ' i P Q :
     C P Q →
-    TransformPersistentEnv M C Γ Γ' →
-    TransformPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
+    TransformIntuitionisticEnv M C Γ Γ' →
+    TransformIntuitionisticEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
   Proof.
     intros ? [HΓ Hwf Hdom]; split; simpl.
     - intros HC Hand. rewrite intuitionistically_and HC // HΓ //.
@@ -758,9 +758,9 @@ Section tac_modal_intro.
     - inversion 1; constructor; auto.
     - intros j. destruct (ident_beq _ _); naive_solver.
   Qed.
-  Global Instance transform_persistent_env_snoc_not (C : PROP2 → PROP1 → Prop) Γ Γ' i P :
-    TransformPersistentEnv M C Γ Γ' →
-    TransformPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
+  Global Instance transform_intuitionistic_env_snoc_not (C : PROP2 → PROP1 → Prop) Γ Γ' i P :
+    TransformIntuitionisticEnv M C Γ Γ' →
+    TransformIntuitionisticEnv M C (Esnoc Γ i P) Γ' | 100.
   Proof.
     intros [HΓ Hwf Hdom]; split; simpl.
     - intros HC Hand. by rewrite and_elim_r HΓ.
@@ -804,7 +804,7 @@ Section tac_modal_intro.
   (** The actual introduction tactic *)
   Lemma tac_modal_intro {A} (sel : A) Γp Γs n Γp' Γs' Q Q' fi :
     FromModal M sel Q' Q →
-    IntoModalPersistentEnv M Γp Γp' (modality_intuitionistic_action M) →
+    IntoModalIntuitionisticEnv M Γp Γp' (modality_intuitionistic_action M) →
     IntoModalSpatialEnv M Γs Γs' (modality_spatial_action M) fi →
     (if fi then Absorbing Q' else TCTrue) →
     envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
@@ -897,8 +897,8 @@ Qed.
 (** The class [MaybeIntoLaterNEnvs] is used by tactics that need to introduce
 laters, e.g. the symbolic execution tactics. *)
 Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
-  into_later_persistent :
-    TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n)
+  into_later_intuitionistic :
+    TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n)
       (env_intuitionistic Δ1) (env_intuitionistic Δ2);
   into_later_spatial :
     TransformSpatialEnv (modality_laterN n)
@@ -906,7 +906,7 @@ Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs PROP) := {
 }.
 
 Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 m :
-  TransformPersistentEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
+  TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
   TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
   MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
 Proof. by split. Qed.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index a62d78783..562f4a85f 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -255,29 +255,29 @@ Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP
   | None => P ← env_lookup i Γs; Some (false, P)
   end.
 
-Definition envs_delete {PROP} (remove_persistent : bool)
+Definition envs_delete {PROP} (remove_intuitionistic : bool)
     (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
   let (Γp,Γs,n) := Δ in
   match p with
-  | true => Envs (if remove_persistent then env_delete i Γp else Γp) Γs n
+  | true => Envs (if remove_intuitionistic then env_delete i Γp else Γp) Γs n
   | false => Envs Γp (env_delete i Γs) n
   end.
 
-Definition envs_lookup_delete {PROP} (remove_persistent : bool)
+Definition envs_lookup_delete {PROP} (remove_intuitionistic : bool)
     (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
   let (Γp,Γs,n) := Δ in
   match env_lookup_delete i Γp with
-  | Some (P,Γp') => Some (true, P, Envs (if remove_persistent then Γp' else Γp) Γs n)
+  | Some (P,Γp') => Some (true, P, Envs (if remove_intuitionistic then Γp' else Γp) Γs n)
   | None => ''(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
   end.
 
-Fixpoint envs_lookup_delete_list {PROP} (remove_persistent : bool)
+Fixpoint envs_lookup_delete_list {PROP} (remove_intuitionistic : bool)
     (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
   match js with
   | [] => Some (true, [], Δ)
   | j :: js =>
-     ''(p,P,Δ') ← envs_lookup_delete remove_persistent j Δ;
-     ''(q,Ps,Δ'') ← envs_lookup_delete_list remove_persistent js Δ';
+     ''(p,P,Δ') ← envs_lookup_delete remove_intuitionistic j Δ;
+     ''(q,Ps,Δ'') ← envs_lookup_delete_list remove_intuitionistic js Δ';
      Some ((p:bool) && q, P :: Ps, Δ'')
   end.
 
@@ -313,7 +313,7 @@ Definition env_spatial_is_nil {PROP} (Δ : envs PROP) : bool :=
 Definition envs_clear_spatial {PROP} (Δ : envs PROP) : envs PROP :=
   Envs (env_intuitionistic Δ) Enil (env_counter Δ).
 
-Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
+Definition envs_clear_intuitionistic {PROP} (Δ : envs PROP) : envs PROP :=
   Envs Enil (env_spatial Δ) (env_counter Δ).
 
 Definition envs_incr_counter {PROP} (Δ : envs PROP) : envs PROP :=
@@ -396,7 +396,7 @@ Global Instance envs_entails_flip_mono :
   Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails PROP).
 Proof. rewrite envs_entails_eq=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
 
-Lemma envs_delete_persistent Δ i : envs_delete false i true Δ = Δ.
+Lemma envs_delete_intuitionistic Δ i : envs_delete false i true Δ = Δ.
 Proof. by destruct Δ. Qed.
 Lemma envs_delete_spatial Δ i :
   envs_delete false i false Δ = envs_delete true i false Δ.
@@ -433,7 +433,7 @@ Lemma envs_lookup_sound Δ i p P :
   envs_lookup i Δ = Some (p,P) →
   of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete true i p Δ).
 Proof. apply envs_lookup_sound'. Qed.
-Lemma envs_lookup_persistent_sound Δ i P :
+Lemma envs_lookup_intuitionistic_sound Δ i P :
   envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
 Proof. intros ?%(envs_lookup_sound' _ false). by destruct Δ. Qed.
 Lemma envs_lookup_sound_2 Δ i p P :
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index b15ae8b9d..1e76c78fe 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -100,11 +100,11 @@ with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
   | TFrame :: TName s :: ts => parse_clear ts (StPat (IClearFrame (SelIdent s)) :: k)
   | TFrame :: TPure :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: k)
-  | TFrame :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelPersistent) :: k)
+  | TFrame :: TAlways :: ts => parse_clear ts (StPat (IClearFrame SelIntuitionistic) :: k)
   | TFrame :: TSep :: ts => parse_clear ts (StPat (IClearFrame SelSpatial) :: k)
   | TName s :: ts => parse_clear ts (StPat (IClear (SelIdent s)) :: k)
   | TPure :: ts => parse_clear ts (StPat (IClear SelPure) :: k)
-  | TAlways :: ts => parse_clear ts (StPat (IClear SelPersistent) :: k)
+  | TAlways :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
   | TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
   | TBraceR :: ts => parse_go ts k
   | _ => None
@@ -148,25 +148,25 @@ Ltac parse_one s :=
   end.
 End intro_pat.
 
-Fixpoint intro_pat_persistent (p : intro_pat) :=
+Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
   match p with
   | IPureElim => true
   | IAlwaysElim _ => true
-  | IList pps => forallb (forallb intro_pat_persistent) pps
+  | IList pps => forallb (forallb intro_pat_intuitionistic) pps
   | ISimpl => true
   | IClear _ => true
   | IClearFrame _ => true
   | _ => false
   end.
 
-Ltac intro_pat_persistent p :=
+Ltac intro_pat_intuitionistic p :=
   lazymatch type of p with
-  | intro_pat => eval cbv in (intro_pat_persistent p)
-  | list intro_pat => eval cbv in (forallb intro_pat_persistent p)
+  | intro_pat => eval cbv in (intro_pat_intuitionistic p)
+  | list intro_pat => eval cbv in (forallb intro_pat_intuitionistic p)
   | string =>
      let pat := intro_pat.parse p in
-     eval cbv in (forallb intro_pat_persistent pat)
+     eval cbv in (forallb intro_pat_intuitionistic pat)
   | ident => false
   | bool => p
-  | ?X => fail "intro_pat_persistent:" p "has unexpected type" X
+  | ?X => fail "intro_pat_intuitionistic:" p "has unexpected type" X
   end.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c35f5c6fa..d9022ec2c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -148,9 +148,9 @@ Local Ltac iElaborateSelPat_go pat Δ Hs :=
   lazymatch pat with
   | [] => eval cbv in Hs
   | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)
-  | SelPersistent :: ?pat =>
+  | SelIntuitionistic :: ?pat =>
     let Hs' := pm_eval (env_dom (env_intuitionistic Δ)) in
-    let Δ' := pm_eval (envs_clear_persistent Δ) in
+    let Δ' := pm_eval (envs_clear_intuitionistic Δ) in
     iElaborateSelPat_go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
   | SelSpatial :: ?pat =>
     let Hs' := pm_eval (env_dom (env_spatial Δ)) in
@@ -249,18 +249,18 @@ Tactic Notation "iAssumption" :=
 (** * False *)
 Tactic Notation "iExFalso" := apply tac_ex_falso.
 
-(** * Making hypotheses persistent or pure *)
-Local Tactic Notation "iPersistent" constr(H) :=
-  eapply tac_persistent with _ H _ _ _; (* (i:=H) *)
+(** * Making hypotheses intuitionistic or pure *)
+Local Tactic Notation "iIntuitionistic" constr(H) :=
+  eapply tac_intuitionistic with _ H _ _ _; (* (i:=H) *)
     [pm_reflexivity ||
      let H := pretty_ident H in
-     fail "iPersistent:" H "not found"
+     fail "iIntuitionistic:" H "not found"
     |iSolveTC ||
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
-     fail "iPersistent:" P "not persistent"
+     fail "iIntuitionistic:" P "not persistent"
     |pm_reduce; iSolveTC ||
      let P := match goal with |- TCOr (Affine ?P) _ => P end in
-     fail "iPersistent:" P "not affine and the goal not absorbing"
+     fail "iIntuitionistic:" P "not affine and the goal not absorbing"
     |pm_reflexivity|].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
@@ -320,7 +320,7 @@ Local Ltac iFrameHyp H :=
 Local Ltac iFrameAnyPure :=
   repeat match goal with H : _ |- _ => iFramePure H end.
 
-Local Ltac iFrameAnyPersistent :=
+Local Ltac iFrameAnyIntuitionistic :=
   iStartProof;
   let rec go Hs :=
     match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
@@ -365,7 +365,7 @@ Local Ltac iFrame_go Hs :=
   lazymatch Hs with
   | [] => idtac
   | SelPure :: ?Hs => iFrameAnyPure; iFrame_go Hs
-  | SelPersistent :: ?Hs => iFrameAnyPersistent; iFrame_go Hs
+  | SelIntuitionistic :: ?Hs => iFrameAnyIntuitionistic; iFrame_go Hs
   | SelSpatial :: ?Hs => iFrameAnySpatial; iFrame_go Hs
   | SelIdent ?H :: ?Hs => iFrameHyp H; iFrame_go Hs
   end.
@@ -446,7 +446,7 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
   iStartProof;
   first
   [(* (?P → _) *)
-   eapply tac_impl_intro_persistent with _ H _ _ _; (* (i:=H) *)
+   eapply tac_impl_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
      [iSolveTC
      |iSolveTC ||
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
@@ -456,11 +456,11 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
       fail 1 "iIntro:" H "not fresh"
      |(* subgoal *)]
   |(* (?P -∗ _) *)
-   eapply tac_wand_intro_persistent with _ H _ _ _; (* (i:=H) *)
+   eapply tac_wand_intro_intuitionistic with _ H _ _ _; (* (i:=H) *)
      [iSolveTC
      |iSolveTC ||
       let P := match goal with |- IntoPersistent _ ?P _ => P end in
-      fail 1 "iIntro:" P "not persistent"
+      fail 1 "iIntro:" P "not intuitionistic"
      |iSolveTC ||
       let P := match goal with |- TCOr (Affine ?P) _ => P end in
       fail 1 "iIntro:" P "not affine and the goal not absorbing"
@@ -665,8 +665,8 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reflexivity
          |solve_done d (*goal*)
          |iSpecializePat_go H1 pats]
-    | SGoal (SpecGoal GPersistent false ?Hs_frame [] ?d) :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
+    | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
+       notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -678,8 +678,8 @@ Ltac iSpecializePat_go H1 pats :=
          |pm_reflexivity
          |iFrame Hs_frame; solve_done d (*goal*)
          |iSpecializePat_go H1 pats]
-    | SGoal (SpecGoal GPersistent _ _ _ _) :: ?pats =>
-       fail "iSpecialize: cannot select hypotheses for persistent premise"
+    | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
+       fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
     | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
        let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
        notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
@@ -696,8 +696,8 @@ Ltac iSpecializePat_go H1 pats :=
           fail "iSpecialize: hypotheses" Hs' "not found"
          |iFrame Hs_frame; solve_done d (*goal*)
          |iSpecializePat_go H1 pats]
-    | SAutoFrame GPersistent :: ?pats =>
-       notypeclasses refine (tac_specialize_assert_persistent _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
+    | SAutoFrame GIntuitionistic :: ?pats =>
+       notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H1 := pretty_ident H1 in
           fail "iSpecialize:" H1 "not found"
@@ -730,7 +730,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
   let pats := spec_pat.parse pat in iSpecializePat_go H pats.
 
 (* The argument [p] denotes whether the conclusion of the specialized term is
-persistent. If so, one can use all spatial hypotheses for both proving the
+intuitionistic. If so, one can use all spatial hypotheses for both proving the
 premises and the remaning goal. The argument [p] can either be a Boolean or an
 introduction pattern, which will be coerced into [true] when it solely contains
 `#` or `%` patterns at the top-level.
@@ -740,7 +740,7 @@ should be kept for one of the premises (i.e. [>[H1 .. Hn]] is used) then [p]
 defaults to [false] (i.e. spatial hypotheses are not preserved). *)
 Tactic Notation "iSpecializeCore" open_constr(H)
     "with" open_constr(xs) open_constr(pat) "as" constr(p) :=
-  let p := intro_pat_persistent p in
+  let p := intro_pat_intuitionistic p in
   let pat := spec_pat.parse pat in
   let H :=
     lazymatch type of H with
@@ -750,11 +750,11 @@ Tactic Notation "iSpecializeCore" open_constr(H)
   iSpecializeArgs H xs; [..|
   lazymatch type of H with
   | ident =>
-    (* The lemma [tac_specialize_persistent_helper] allows one to use all
+    (* The lemma [tac_specialize_intuitionistic_helper] allows one to use all
     spatial hypotheses for both proving the premises of the lemma we
     specialize as well as those of the remaining goal. We can only use it when
-    the result of the specialization is persistent, and no modality is
-    eliminated. We do not use [tac_specialize_persistent_helper] in the case
+    the result of the specialization is intuitionistic, and no modality is
+    eliminated. We do not use [tac_specialize_intuitionistic_helper] in the case
     only universal quantifiers and no implications or wands are instantiated
     (i.e [pat = []]) because it is a.) not needed, and b.) more efficient. *)
     let pat := spec_pat.parse pat in
@@ -762,13 +762,13 @@ Tactic Notation "iSpecializeCore" open_constr(H)
       (p && bool_decide (pat ≠ []) && negb (existsb spec_pat_modal pat)) with
     | true =>
        (* FIXME: do something reasonable when the BI is not affine *)
-       notypeclasses refine (tac_specialize_persistent_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
+       notypeclasses refine (tac_specialize_intuitionistic_helper _ _ H _ _ _ _ _ _ _ _ _ _ _);
          [pm_reflexivity ||
           let H := pretty_ident H in
           fail "iSpecialize:" H "not found"
          |iSpecializePat H pat;
            [..
-           |notypeclasses refine (tac_specialize_persistent_helper_done _ H _ _ _);
+           |notypeclasses refine (tac_specialize_intuitionistic_helper_done _ H _ _ _);
             pm_reflexivity]
          |iSolveTC ||
           let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
@@ -1112,10 +1112,10 @@ Tactic Notation "iModIntro" uconstr(sel) :=
     [iSolveTC ||
      fail "iModIntro: the goal is not a modality"
     |iSolveTC ||
-     let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+     let s := lazymatch goal with |- IntoModalIntuitionisticEnv _ _ _ ?s => s end in
      lazymatch eval hnf in s with
-     | MIEnvForall ?C => fail "iModIntro: persistent context does not satisfy" C
-     | MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
+     | MIEnvForall ?C => fail "iModIntro: intuitionistic context does not satisfy" C
+     | MIEnvIsEmpty => fail "iModIntro: intuitionistic context is non-empty"
      end
     |iSolveTC ||
      let s := lazymatch goal with |- IntoModalSpatialEnv _ _ _ ?s _ => s end in
@@ -1166,7 +1166,7 @@ Local Ltac iDestructHypGo Hz pat :=
   | IPureElim => iPure Hz as ?
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
-  | IAlwaysElim ?pat => iPersistent Hz; iDestructHypGo Hz pat
+  | IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
   | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
   | _ => fail "iDestruct:" pat "invalid"
   end.
@@ -1590,7 +1590,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   | _ =>
      (* Only copy the hypothesis in case there is a [CopyDestruct] instance.
      Also, rule out cases in which it does not make sense to copy, namely when
-     destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
+     destructing a lemma (instead of a hypothesis) or a spatial hypothesis
      (which cannot be kept). *)
      iStartProof;
      lazymatch ident with
@@ -1601,7 +1601,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
           let H := pretty_ident H in
           fail "iDestruct:" H "not found"
         | Some (true, ?P) =>
-           (* persistent hypothesis, check for a CopyDestruct instance *)
+           (* intuitionistic hypothesis, check for a CopyDestruct instance *)
            tryif (let dummy := constr:(_ : CopyDestruct P) in idtac)
            then (iPoseProofCore lem as p false tac)
            else (iSpecializeCore lem as p; [..| tac H])
@@ -1688,14 +1688,14 @@ Tactic Notation "iPoseProof" open_constr(lem) "as" "(" simple_intropattern(x1)
 result in the following actions:
 
 - Revert the proofmode hypotheses [Hs]
-- Revert all remaining spatial hypotheses and the remaining persistent
+- Revert all remaining spatial hypotheses and the remaining intuitionistic
   hypotheses containing the induction variable [x]
 - Revert the pure hypotheses [x1..xn]
 
 - Actuall perform induction
 
 - Introduce thee pure hypotheses [x1..xn]
-- Introduce the spatial hypotheses and persistent hypotheses involving [x]
+- Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
 - Introduce the proofmode hypotheses [Hs]
 *)
 Tactic Notation "iInductionCore" tactic(tac) "as" constr(IH) :=
@@ -1982,7 +1982,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
     |iSpecializeCore H with hnil pats as p; [..|tac H]].
 
 Tactic Notation "iAssertCore" open_constr(Q) "as" constr(p) tactic(tac) :=
-  let p := intro_pat_persistent p in
+  let p := intro_pat_intuitionistic p in
   lazymatch p with
   | true => iAssertCore Q with "[#]" as p tac
   | false => iAssertCore Q with "[]" as p tac
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 51ccf1ead..0db1e202a 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -12,7 +12,7 @@ Declare Reduction pm_eval := cbv [
   env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
   envs_simple_replace envs_replace envs_split
-  envs_clear_spatial envs_clear_persistent envs_incr_counter
+  envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
   envs_split_go envs_split env_to_prop
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 6d7710d6e..f014853f5 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 
 Inductive sel_pat :=
   | SelPure
-  | SelPersistent
+  | SelIntuitionistic
   | SelSpatial
   | SelIdent : ident → sel_pat.
 
@@ -21,7 +21,7 @@ Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :
   | [] => Some (reverse k)
   | TName s :: ts => parse_go ts (SelIdent s :: k)
   | TPure :: ts => parse_go ts (SelPure :: k)
-  | TAlways :: ts => parse_go ts (SelPersistent :: k)
+  | TAlways :: ts => parse_go ts (SelIntuitionistic :: k)
   | TSep :: ts => parse_go ts (SelSpatial :: k)
   | _ => None
   end.
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index dd93c0ebe..2332ebac5 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -2,7 +2,7 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import base tokens.
 Set Default Proof Using "Type".
 
-Inductive goal_kind := GSpatial | GModal | GPersistent.
+Inductive goal_kind := GSpatial | GModal | GIntuitionistic.
 
 Record spec_goal := SpecGoal {
   spec_goal_kind : goal_kind;
@@ -38,14 +38,14 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
   | [] => Some (reverse k)
   | TName s :: ts => parse_go ts (SIdent s :: k)
   | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
-     parse_go ts (SAutoFrame GPersistent :: k)
+     parse_go ts (SAutoFrame GIntuitionistic :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GSpatial :: k)
   | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GModal :: k)
   | TBracketL :: TPure :: TBracketR :: ts => parse_go ts (SPureGoal false :: k)
   | TBracketL :: TPure :: TDone :: TBracketR :: ts => parse_go ts (SPureGoal true :: k)
-  | TBracketL :: TAlways :: ts => parse_goal ts GPersistent false [] [] k
+  | TBracketL :: TAlways :: ts => parse_goal ts GIntuitionistic false [] [] k
   | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
   | TBracketL :: ts => parse_goal ts GSpatial false [] [] k
   | TForall :: ts => parse_go ts (SForall :: k)
-- 
GitLab