diff --git a/CHANGELOG.md b/CHANGELOG.md
index ddbf57c520b64567aab2fa5c9e5eaeb179a2f3d9..455986f07962980a04e6c6aa356f3b7d6267f275 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   + `singleton_includedN` → `singleton_includedN_l`.
   + `singleton_included` → `singleton_included_l`.
   + `singleton_included_exclusive` → `singleton_included_exclusive_l`
+* The proof mode now supports names for pure facts in intro patterns. Support
+  requires implementing `string_to_ident` with either a plugin or Ltac2, which
+  only work on Coq 8.10 and Coq 8.11 respectively. Without this tactic such
+  patterns will fail.
 
 **Changes in heap_lang:**
 
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 6643f7b8118fbd7923adb0231fcf18c1603d1164..3b5776176f25a7c8d051a5c8b27588944ac51776 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -615,3 +615,21 @@ Tactic failure: iRevert: k is used in hypothesis "Hk".
      : string
 The command has indeed failed with message:
 Tactic failure: iLöb: not a step-indexed BI entailment.
+"test_pure_name"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  P1 : PROP
+  P2, P3 : Prop
+  Himpl : P2 → P3
+  HP2 : P2
+  ============================
+  "HP" : P1
+  --------------------------------------∗
+  P1 ∗ ⌜P3⌝
+  
+"test_not_fresh"
+     : string
+The command has indeed failed with message:
+H is already used.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b92a17884c37fb343e42b2dad58dd43d58011b6c..f4fefc0a57d41df816a19004e8b407f0ce9504ab 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -54,6 +54,14 @@ Lemma demo_3 P1 P2 P3 :
   P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
 Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
 
+Lemma test_pure_space_separated P1 :
+  <affine> ⌜True⌝ ∗ P1 -∗ P1.
+Proof.
+  (* [% H] should be parsed as two separate patterns and not the pure name
+  [H] *)
+  iIntros "[% H] //".
+Qed.
+
 Definition foo (P : PROP) := (P -∗ P)%I.
 Definition bar : PROP := (∀ P, foo P)%I.
 
@@ -1071,3 +1079,34 @@ Check "iLöb_no_sbi".
 Lemma iLöb_no_sbi P : ⊢ P.
 Proof. Fail iLöb as "IH". Abort.
 End error_tests_bi.
+
+Section pure_name_tests.
+Context {PROP : sbi}.
+Implicit Types P Q R : PROP.
+(* mock string_to_ident for just these tests *)
+Ltac ltac_tactics.string_to_ident_hook ::=
+  make_string_to_ident_hook ltac:(fun s => lazymatch s with
+                                        | "HP2" => ident:(HP2)
+                                        | "H" => ident:(H)
+                                        | _ => fail 100 s
+                                        end).
+
+Check "test_pure_name".
+Lemma test_pure_name P1 (P2 P3: Prop) (Himpl: P2 -> P3) :
+  P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P3⌝.
+Proof.
+  iIntros "[HP %HP2]".
+  Show.
+  iFrame.
+  iPureIntro.
+  exact (Himpl HP2).
+Qed.
+
+Check "test_not_fresh".
+Lemma test_not_fresh P1 (P2: Prop) (H:P2) :
+  P1 ∗ ⌜P2⌝ -∗ P1 ∗ ⌜P2⌝.
+Proof.
+  Fail iIntros "[H %H]".
+Abort.
+
+End pure_name_tests.
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 0227092dbdb2e55d7643f39d806b5cd3c9f869d2..041c655ef65b9cda4e63d78344617465ad73a609 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -2,13 +2,17 @@ From stdpp Require Export strings.
 From iris.proofmode Require Import base tokens sel_patterns.
 Set Default Proof Using "Type".
 
+Inductive gallina_ident :=
+  | IGallinaNamed : string → gallina_ident
+  | IGallinaAnon : gallina_ident.
+
 Inductive intro_pat :=
   | IIdent : ident → intro_pat
   | IFresh : intro_pat
   | IDrop : intro_pat
   | IFrame : intro_pat
   | IList : list (list intro_pat) → intro_pat
-  | IPure : intro_pat
+  | IPure : gallina_ident → intro_pat
   | IIntuitionistic : intro_pat → intro_pat
   | ISpatial : intro_pat → intro_pat
   | IModalElim : intro_pat → intro_pat
@@ -84,7 +88,8 @@ 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 IPure :: k)
+  | TPure (Some s) :: ts => parse_go ts (StPat (IPure (IGallinaNamed s)) :: k)
+  | TPure None :: ts => parse_go ts (StPat (IPure IGallinaAnon) :: k)
   | TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
   | TMinus :: TIntuitionistic :: ts => parse_go ts (StSpatial :: k)
   | TModal :: ts => parse_go ts (StModalElim :: k)
@@ -101,11 +106,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
 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 :: TPure None :: ts => parse_clear ts (StPat (IClearFrame SelPure) :: 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)
+  | TPure None :: ts => parse_clear ts (StPat (IClear SelPure) :: 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
@@ -153,7 +158,7 @@ End intro_pat.
 
 Fixpoint intro_pat_intuitionistic (p : intro_pat) :=
   match p with
-  | IPure => true
+  | IPure _ => true
   | IIntuitionistic _ => true
   | IList pps => forallb (forallb intro_pat_intuitionistic) pps
   | ISimpl => true
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 7a5976c5b5fc184864598dca499577ac1724f3b5..04a2ecb30e6f59321564fcbcb9e4c39739ecebc8 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1383,6 +1383,30 @@ Tactic Notation "iModCore" constr(H) :=
     |iSolveSideCondition
     |pm_reduce; pm_prettify(* subgoal *)].
 
+(* This tactic should take a string [s] and solve the goal with [exact (λ
+(s:unit), tt)], where the name of the binder is the string as an identifier.
+We use this API (rather than simply returning the identifier) since it works
+correctly when replaced with [fail].
+
+One way to implement such a function is to use Ltac2 on Coq 8.11+. Another
+option is https://github.com/ppedrot/coq-string-ident for Coq 8.10. *)
+Ltac string_to_ident_hook := fun s => fail 100 "string_to_ident is unavailable in this version of Coq".
+
+(* Turn a string_to_ident that produces an ident value into one that solves the
+goal with a [unit → unit] function instead, as expected for
+[string_to_ident_hook]. *)
+Ltac make_string_to_ident_hook string_to_ident :=
+  fun s => let x := string_to_ident s in
+        exact (fun (x:unit) => tt).
+
+(* [string_to_ident] uses [string_to_ident_hook] to turn [s] into an identifier
+and return it. *)
+Local Ltac string_to_ident s :=
+  let ident_fun := constr:(ltac:(string_to_ident_hook s)) in
+  lazymatch ident_fun with
+  | λ (x:_), _ => x
+  end.
+
 (** * Basic destruct tactic *)
 Local Ltac iDestructHypGo Hz pat :=
   lazymatch pat with
@@ -1400,7 +1424,9 @@ 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]
-  | IPure => iPure Hz as ?
+  | IPure IGallinaAnon => iPure Hz as ?
+  | IPure (IGallinaNamed ?s) => let x := string_to_ident s in
+                                iPure Hz as x
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
   | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index ca44ac01b3b1993cdf18bb5d6919c3ace2313c41..aac295086d279447dbe4fea413a514496a81676a 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -20,7 +20,7 @@ Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :
   match ts with
   | [] => Some (reverse k)
   | TName s :: ts => parse_go ts (SelIdent s :: k)
-  | TPure :: ts => parse_go ts (SelPure :: k)
+  | TPure None :: ts => parse_go ts (SelPure :: k)
   | TIntuitionistic :: ts => parse_go ts (SelIntuitionistic :: k)
   | TSep :: ts => parse_go ts (SelSpatial :: k)
   | _ => None
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index a3a7d44198cb4c6dc4aa2b6c6a7aa0d9c0d484af..2da6bf52c313438a7e58e496c8edcf4e6cbd0bcb 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -60,9 +60,9 @@ Fixpoint parse_go (ts : list token) (k : stack) : option (list spec_pat) :=
      parse_go ts (StPat (SAutoFrame GSpatial) :: k)
   | TBracketL :: TModal :: TFrame :: TBracketR :: ts =>
      parse_go ts (StPat (SAutoFrame GModal) :: k)
-  | TBracketL :: TPure :: TBracketR :: ts =>
+  | TBracketL :: TPure None :: TBracketR :: ts =>
      parse_go ts (StPat (SPureGoal false) :: k)
-  | TBracketL :: TPure :: TDone :: TBracketR :: ts =>
+  | TBracketL :: TPure None :: TDone :: TBracketR :: ts =>
      parse_go ts (StPat (SPureGoal true) :: k)
   | TBracketL :: TIntuitionistic :: ts => parse_goal ts GIntuitionistic false [] [] k
   | TBracketL :: TModal :: ts => parse_goal ts GModal false [] [] k
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index 1ceb2e53f41ea0dd46b4520b3c234e8d1d945237..cb3a34fbf48686d59737563b618a065be51c65c3 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -14,7 +14,7 @@ Inductive token :=
   | TParenR : token
   | TBraceL : token
   | TBraceR : token
-  | TPure : token
+  | TPure : option string → token
   | TIntuitionistic : token
   | TModal : token
   | TPureIntro : token
@@ -31,12 +31,14 @@ Inductive token :=
 Inductive state :=
   | SName : string → state
   | SNat : nat → state
+  | SPure : string -> state
   | SNone : state.
 
 Definition cons_state (kn : state) (k : list token) : list token :=
   match kn with
   | SNone => k
   | SName s => TName (string_rev s) :: k
+  | SPure s => TPure (if String.eqb s "" then None else Some (string_rev s)) :: k
   | SNat n => TNat n :: k
   end.
 
@@ -53,7 +55,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   | String "&" s => tokenize_go s (TAmp :: cons_state kn k) SNone
   | 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 (cons_state kn k) (SPure "")
   | 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
@@ -83,6 +85,7 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
         | None => tokenize_go s k (SName (String a ""))
         end
      | SName s' => tokenize_go s k (SName (String a s'))
+     | SPure s' => tokenize_go s k (SPure (String a s'))
      | SNat n =>
         match is_nat a with
         | Some n' => tokenize_go s k (SNat (n' + 10 * n))