diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index aadc9a54f6e0661775b4a5bbb23efe4e14d7e227..1857119891e963c5349d74606f8d332a6b92bbc8 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -8,12 +8,11 @@ Inductive intro_pat :=
   | IDrop : intro_pat
   | IFrame : intro_pat
   | IList : list (list intro_pat) → intro_pat
-  | IPureElim : intro_pat
-  | IAlwaysElim : intro_pat → intro_pat
+  | IPure : intro_pat
+  | IIntuitionistic : intro_pat → intro_pat
   | IModalElim : intro_pat → intro_pat
   | IRewrite : direction → intro_pat
   | IPureIntro : intro_pat
-  | IAlwaysIntro : intro_pat
   | IModalIntro : intro_pat
   | ISimpl : intro_pat
   | IDone : intro_pat
@@ -29,7 +28,7 @@ Inductive stack_item :=
   | StConjList : stack_item
   | StBar : stack_item
   | StAmp : stack_item
-  | StAlwaysElim : stack_item
+  | StIntuitionistic : stack_item
   | StModalElim : stack_item.
 Notation stack := (list stack_item).
 
@@ -38,8 +37,8 @@ Fixpoint close_list (k : stack)
   match k with
   | StList :: k => Some (StPat (IList (ps :: pss)) :: k)
   | StPat pat :: k => close_list k (pat :: ps) pss
-  | StAlwaysElim :: k =>
-     ''(p,ps) ← maybe2 (::) ps; close_list k (IAlwaysElim p :: ps) pss
+  | StIntuitionistic :: k =>
+     ''(p,ps) ← maybe2 (::) ps; close_list k (IIntuitionistic p :: ps) pss
   | StModalElim :: k =>
      ''(p,ps) ← maybe2 (::) ps; close_list k (IModalElim p :: ps) pss
   | StBar :: k => close_list k [] (ps :: pss)
@@ -63,7 +62,7 @@ Fixpoint close_conj_list (k : stack)
           end;
      Some (StPat (big_conj ps) :: k)
   | StPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
-  | StAlwaysElim :: k => p ← cur; close_conj_list k (Some (IAlwaysElim p)) ps
+  | StIntuitionistic :: k => p ← cur; close_conj_list k (Some (IIntuitionistic p)) ps
   | StModalElim :: k => p ← cur; close_conj_list k (Some (IModalElim p)) ps
   | StAmp :: k => p ← cur; close_conj_list k None (p :: ps)
   | _ => None
@@ -82,13 +81,12 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TParenL :: ts => parse_go ts (StConjList :: k)
   | TAmp :: ts => parse_go ts (StAmp :: k)
   | TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
-  | TPure :: ts => parse_go ts (StPat IPureElim :: k)
-  | TAlways :: ts => parse_go ts (StAlwaysElim :: k)
+  | TPure :: ts => parse_go ts (StPat IPure :: k)
+  | TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
   | TModal :: ts => parse_go ts (StModalElim :: k)
   | TArrow d :: ts => parse_go ts (StPat (IRewrite d) :: k)
   | TPureIntro :: ts => parse_go ts (StPat IPureIntro :: k)
-  | TAlwaysIntro :: ts => parse_go ts (StPat IAlwaysIntro :: k)
-  | TModalIntro :: ts => parse_go ts (StPat IModalIntro :: k)
+  | (TModalIntro | TIntuitionisticIntro) :: ts => parse_go ts (StPat IModalIntro :: k)
   | TSimpl :: ts => parse_go ts (StPat ISimpl :: k)
   | TDone :: ts => parse_go ts (StPat IDone :: k)
   | TAll :: ts => parse_go ts (StPat IAll :: k)
@@ -100,11 +98,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 SelIntuitionistic) :: k)
+  | TFrame :: TIntuitionistic :: 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 SelIntuitionistic) :: k)
+  | TIntuitionistic :: ts => parse_clear ts (StPat (IClear SelIntuitionistic) :: k)
   | TSep :: ts => parse_clear ts (StPat (IClear SelSpatial) :: k)
   | TBraceR :: ts => parse_go ts k
   | _ => None
@@ -114,7 +112,7 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
   match k with
   | [] => Some ps
   | StPat pat :: k => close k (pat :: ps)
-  | StAlwaysElim :: k => ''(p,ps) ← maybe2 (::) ps; close k (IAlwaysElim p :: ps)
+  | StIntuitionistic :: k => ''(p,ps) ← maybe2 (::) ps; close k (IIntuitionistic p :: ps)
   | StModalElim :: k => ''(p,ps) ← maybe2 (::) ps; close k (IModalElim p :: ps)
   | _ => None
   end.
@@ -150,8 +148,8 @@ End intro_pat.
 
 Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
   match p with
-  | IPureElim => true
-  | IAlwaysElim _ => true
+  | IPure => true
+  | IIntuitionistic _ => true
   | IList pps => forallb (forallb intro_pat_intuitionistic) pps
   | ISimpl => true
   | IClear _ => true
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 5fdeb14cc77258d73d0913264daf06ef0db9f441..75d192389d9f7e355620a6795897770a209cb8ad 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1375,10 +1375,10 @@ Local Ltac iDestructHypGo Hz pat :=
   | IList [[?pat1; ?pat2]] =>
      let Hy := iFresh in iAndDestruct Hz as Hz Hy; iDestructHypGo Hz pat1; iDestructHypGo Hy pat2
   | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [iDestructHypGo Hz pat1|iDestructHypGo Hz pat2]
-  | IPureElim => iPure Hz as ?
+  | IPure => iPure Hz as ?
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
-  | IAlwaysElim ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
+  | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
   | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
   | _ => fail "iDestruct:" pat "invalid"
   end.
@@ -1473,13 +1473,12 @@ Ltac iIntros_go pats startproof :=
     | false => idtac
     end
   (* Optimizations to avoid generating fresh names *)
-  | IPureElim :: ?pats => iIntro (?); iIntros_go pats startproof
-  | IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
+  | IPure :: ?pats => iIntro (?); iIntros_go pats startproof
+  | IIntuitionistic (IIdent ?H) :: ?pats => iIntro #H; iIntros_go pats false
   | IDrop :: ?pats => iIntro _; iIntros_go pats startproof
   | IIdent ?H :: ?pats => iIntro H; iIntros_go pats startproof
   (* Introduction patterns that can only occur at the top-level *)
   | IPureIntro :: ?pats => iPureIntro; iIntros_go pats false
-  | IAlwaysIntro :: ?pats => iAlways; iIntros_go pats false
   | IModalIntro :: ?pats => iModIntro; iIntros_go pats false
   | IForall :: ?pats => repeat iIntroForall; iIntros_go pats startproof
   | IAll :: ?pats => repeat (iIntroForall || iIntro); iIntros_go pats startproof
@@ -1489,7 +1488,7 @@ Ltac iIntros_go pats startproof :=
   | IClearFrame ?H :: ?pats => iFrame H; iIntros_go pats false
   | IDone :: ?pats => try done; iIntros_go pats startproof
   (* Introduction + destruct *)
-  | IAlwaysElim ?pat :: ?pats =>
+  | IIntuitionistic ?pat :: ?pats =>
      let H := iFresh in iIntro #H; iDestructHyp H as pat; iIntros_go pats false
   | ?pat :: ?pats =>
      let H := iFresh in iIntro H; iDestructHyp H as pat; iIntros_go pats false
@@ -2092,7 +2091,7 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
        fix_ihs ltac:(fun j =>
          let IH' := eval vm_compute in
            match j with 0%N => IH | _ => IH +:+ pretty j end in
-         iIntros [IAlwaysElim (IIdent IH')];
+         iIntros [IIntuitionistic (IIdent IH')];
          let j := eval vm_compute in (1 + j)%N in
          rev_tac j)
     | _ => rev_tac 0%N
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index f014853f58d60e1c557f2dd4ee58b0a47e9132fb..ca44ac01b3b1993cdf18bb5d6919c3ace2313c41 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -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 (SelIntuitionistic :: k)
+  | TIntuitionistic :: 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 2c0ca4725b598602c937ac43e765e017b918f6ee..a3a7d44198cb4c6dc4aa2b6c6a7aa0d9c0d484af 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -54,7 +54,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
   | TParenL :: TName s :: ts => parse_go ts (StIdent s :: k)
   | TParenR :: ts => k ← close_ident k []; parse_go ts k
   | TName s :: ts => parse_go ts (StPat (SIdent s []) :: k)
-  | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
+  | TBracketL :: TIntuitionistic :: TFrame :: TBracketR :: ts =>
      parse_go ts (StPat (SAutoFrame GIntuitionistic) :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
      parse_go ts (StPat (SAutoFrame GSpatial) :: k)
@@ -64,7 +64,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
      parse_go ts (StPat (SPureGoal false) :: k)
   | TBracketL :: TPure :: TDone :: TBracketR :: ts =>
      parse_go ts (StPat (SPureGoal true) :: k)
-  | TBracketL :: TAlways :: ts => parse_goal ts GIntuitionistic false [] [] k
+  | TBracketL :: TIntuitionistic :: 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 (StPat SForall :: k)
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index ed3a8b8f8824fef0b09896b24abfb57416dd41fc..1ceb2e53f41ea0dd46b4520b3c234e8d1d945237 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -15,10 +15,10 @@ Inductive token :=
   | TBraceL : token
   | TBraceR : token
   | TPure : token
-  | TAlways : token
+  | TIntuitionistic : token
   | TModal : token
   | TPureIntro : token
-  | TAlwaysIntro : token
+  | TIntuitionisticIntro : token
   | TModalIntro : token
   | TSimpl : token
   | TDone : token
@@ -54,10 +54,10 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   | String "{" s => tokenize_go s (TBraceL :: cons_state kn k) SNone
   | String "}" s => tokenize_go s (TBraceR :: cons_state kn k) SNone
   | String "%" s => tokenize_go s (TPure :: cons_state kn k) SNone
-  | String "#" s => tokenize_go s (TAlways :: cons_state kn k) SNone
+  | String "#" s => tokenize_go s (TIntuitionistic :: cons_state kn k) SNone
   | String ">" s => tokenize_go s (TModal :: cons_state kn k) SNone
   | String "!" (String "%" s) => tokenize_go s (TPureIntro :: cons_state kn k) SNone
-  | String "!" (String "#" s) => tokenize_go s (TAlwaysIntro :: cons_state kn k) SNone
+  | String "!" (String "#" s) => tokenize_go s (TIntuitionisticIntro :: cons_state kn k) SNone
   | String "!" (String ">" s) => tokenize_go s (TModalIntro :: cons_state kn k) SNone
   | String "/" (String "/" (String "=" s)) =>
      tokenize_go s (TSimpl :: TDone :: cons_state kn k) SNone