diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 1608c9a29e941181ae9db80c95ecf686113466dd..8b140f72453a3e8003307a1b281ee04435552bd8 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -92,7 +92,7 @@ End inv.
 Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
   let Htmp := iFresh in
   let patback := intro_pat.parse_one Hclose in
-  let pat := constr:(IList [[IName Htmp; patback]]) in
+  let pat := constr:(IList [[IIdent Htmp; patback]]) in
   iMod (inv_open _ N with "[#]") as pat;
     [idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
     [solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 1bc3e3d16a06e09d99ada1a723a4f582744a323f..bfa226e3c8013cec1606c5ecd3d006fa9b23c923 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -104,7 +104,7 @@ Qed.
 Lemma ownI_open i P : wsat ∗ ownI i P ∗ ownE {[i]} ⊢ wsat ∗ ▷ P ∗ ownD {[i]}.
 Proof.
   rewrite /ownI /wsat -!lock.
-  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
+  iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
   iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
   - iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
@@ -115,7 +115,7 @@ Qed.
 Lemma ownI_close i P : wsat ∗ ownI i P ∗ ▷ P ∗ ownD {[i]} ⊢ wsat ∗ ownE {[i]}.
 Proof.
   rewrite /ownI /wsat -!lock.
-  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
+  iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
   iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
   iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
   - iDestruct (ownD_singleton_twice with "[$]") as %[].
@@ -128,7 +128,7 @@ Lemma ownI_alloc φ P :
   wsat ∗ ▷ P ==∗ ∃ i, ⌜φ i⌝ ∗ wsat ∗ ownI i P.
 Proof.
   iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
-  iDestruct "Hw" as (I) "[? HI]".
+  iDestruct "Hw" as (I) "[Hw HI]".
   iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
   iMod (own_updateP with "[$]") as "HE".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
@@ -150,7 +150,7 @@ Lemma ownI_alloc_open φ P :
   (∀ E : gset positive, ∃ i, i ∉ E ∧ φ i) →
   wsat ==∗ ∃ i, ⌜φ i⌝ ∗ (ownE {[i]} -∗ wsat) ∗ ownI i P ∗ ownD {[i]}.
 Proof.
-  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[? HI]".
+  iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
   iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
   iMod (own_updateP with "[$]") as "HD".
   { apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None ∧ φ i)).
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 4d4d6cba841cbfb687b454444cb7562615f96ab7..7a9f78cd88906256508fae367b401f36579d7ee1 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -153,7 +153,7 @@ Section proof.
     wp_store.
     iDestruct (own_valid_2 with "Hauth Hγo") as
       %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
-    iDestruct "Haown" as "[[Hγo' _]|?]".
+    iDestruct "Haown" as "[[Hγo' _]|Haown]".
     { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
     iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
     { apply auth_update, prod_local_update_1.
diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index 1e185e2cdf4d4b2852b6c2b4b043b47a538d128c..4ff779335013ce517652eda6467683823c1948ec 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -49,3 +49,37 @@ Qed.
 
 Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
 Proof. apply iff_reflect. by rewrite string_beq_true. Qed.
+
+Module Export ident.
+Inductive ident :=
+  | IAnon : positive → ident
+  | INamed :> string → ident.
+End ident.
+
+Instance maybe_IAnon : Maybe IAnon := λ i,
+  match i with IAnon n => Some n | _ => None end.
+Instance maybe_INamed : Maybe INamed := λ i,
+  match i with INamed s => Some s | _ => None end.
+
+Instance beq_eq_dec : EqDecision ident.
+Proof. solve_decision. Defined.
+
+Definition positive_beq := Eval compute in Pos.eqb.
+
+Lemma positive_beq_true x y : positive_beq x y = true ↔ x = y.
+Proof. apply Pos.eqb_eq. Qed.
+
+Definition ident_beq (i1 i2 : ident) : bool :=
+  match i1, i2 with
+  | IAnon n1, IAnon n2 => positive_beq n1 n2
+  | INamed s1, INamed s2 => string_beq s1 s2
+  | _, _ => false
+  end.
+
+Lemma ident_beq_true i1 i2 : ident_beq i1 i2 = true ↔ i1 = i2.
+Proof.
+  destruct i1, i2; rewrite /= ?string_beq_true ?positive_beq_true; naive_solver.
+Qed.
+
+Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
+Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 5867734c7b2d6c798e0a155377dae77de6391042..e0dc64809b031e30073fa73492279896c22c7b0a 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -1,7 +1,6 @@
 From iris.base_logic Require Export base_logic.
 From iris.base_logic Require Import big_op tactics.
 From iris.proofmode Require Export base environments classes.
-From stdpp Require Import stringmap hlist.
 Set Default Proof Using "Type".
 Import uPred.
 Import env_notations.
@@ -36,22 +35,22 @@ Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
   env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Definition envs_dom {M} (Δ : envs M) : list string :=
+Definition envs_dom {M} (Δ : envs M) : list ident :=
   env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
 
-Definition envs_lookup {M} (i : string) (Δ : envs M) : option (bool * uPred M) :=
+Definition envs_lookup {M} (i : ident) (Δ : envs M) : option (bool * uPred M) :=
   let (Γp,Γs) := Δ in
   match env_lookup i Γp with
   | Some P => Some (true, P) | None => P ← env_lookup i Γs; Some (false, P)
   end.
 
-Definition envs_delete {M} (i : string) (p : bool) (Δ : envs M) : envs M :=
+Definition envs_delete {M} (i : ident) (p : bool) (Δ : envs M) : envs M :=
   let (Γp,Γs) := Δ in
   match p with
   | true => Envs (env_delete i Γp) Γs | false => Envs Γp (env_delete i Γs)
   end.
 
-Definition envs_lookup_delete {M} (i : string)
+Definition envs_lookup_delete {M} (i : ident)
     (Δ : envs M) : option (bool * uPred M * envs M) :=
   let (Γp,Γs) := Δ in
   match env_lookup_delete i Γp with
@@ -59,7 +58,7 @@ Definition envs_lookup_delete {M} (i : string)
   | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
   end.
 
-Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : bool)
+Fixpoint envs_lookup_delete_list {M} (js : list ident) (remove_persistent : bool)
     (Δ : envs M) : option (bool * list (uPred M) * envs M) :=
   match js with
   | [] => Some (true, [], Δ)
@@ -71,7 +70,7 @@ Fixpoint envs_lookup_delete_list {M} (js : list string) (remove_persistent : boo
   end.
 
 Definition envs_snoc {M} (Δ : envs M)
-    (p : bool) (j : string) (P : uPred M) : envs M :=
+    (p : bool) (j : ident) (P : uPred M) : envs M :=
   let (Γp,Γs) := Δ in
   if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).
 
@@ -83,7 +82,7 @@ Definition envs_app {M} (p : bool)
   | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs')
   end.
 
-Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
+Definition envs_simple_replace {M} (i : ident) (p : bool) (Γ : env (uPred M))
     (Δ : envs M) : option (envs M) :=
   let (Γp,Γs) := Δ in
   match p with
@@ -91,7 +90,7 @@ Definition envs_simple_replace {M} (i : string) (p : bool) (Γ : env (uPred M))
   | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs')
   end.
 
-Definition envs_replace {M} (i : string) (p q : bool) (Γ : env (uPred M))
+Definition envs_replace {M} (i : ident) (p q : bool) (Γ : env (uPred M))
     (Δ : envs M) : option (envs M) :=
   if eqb p q then envs_simple_replace i p Γ Δ
   else envs_app q Γ (envs_delete i p Δ).
@@ -106,7 +105,7 @@ Definition envs_clear_persistent {M} (Δ : envs M) : envs M :=
   Envs Enil (env_spatial Δ).
 
 Fixpoint envs_split_go {M}
-    (js : list string) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
+    (js : list ident) (Δ1 Δ2 : envs M) : option (envs M * envs M) :=
   match js with
   | [] => Some (Δ1, Δ2)
   | j :: js =>
@@ -117,7 +116,7 @@ Fixpoint envs_split_go {M}
 (* if [d = Right] then [result = (remaining hyps, hyps named js)] and
    if [d = Left] then [result = (hyps named js, remaining hyps)] *)
 Definition envs_split {M} (d : direction)
-    (js : list string) (Δ : envs M) : option (envs M * envs M) :=
+    (js : list ident) (Δ : envs M) : option (envs M * envs M) :=
   '(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
@@ -224,11 +223,11 @@ Proof.
   apply wand_intro_l; destruct p; simpl.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; destruct (string_beq_reflect j i); naive_solver.
+      intros j; destruct (ident_beq_reflect j i); naive_solver.
     + by rewrite persistently_sep assoc.
   - apply sep_intro_True_l; [apply pure_intro|].
     + destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
-      intros j; destruct (string_beq_reflect j i); naive_solver.
+      intros j; destruct (ident_beq_reflect j i); naive_solver.
     + solve_sep_entails.
 Qed.
 
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 5236e5e0966557afc25087ebfa81a07a0e1c26eb..ba0b78129f1d6bb4a68959a0254ceaa2d5a8e18c 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -1,21 +1,19 @@
-From stdpp Require Export strings.
 From iris.proofmode Require Import base.
 From iris.algebra Require Export base.
-From stdpp Require Import stringmap.
 Set Default Proof Using "Type".
 
 Inductive env (A : Type) : Type :=
   | Enil : env A
-  | Esnoc : env A → string → A → env A.
+  | Esnoc : env A → ident → A → env A.
 Arguments Enil {_}.
-Arguments Esnoc {_} _ _%string _.
+Arguments Esnoc {_} _ _ _.
 Instance: Params (@Enil) 1.
 Instance: Params (@Esnoc) 1.
 
-Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
+Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   match Γ with
   | Enil => None
-  | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
+  | Esnoc Γ j x => if ident_beq i j then Some x else env_lookup i Γ
   end.
 
 Module env_notations.
@@ -37,7 +35,7 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
 Coercion env_to_list : env >-> list.
 Instance: Params (@env_to_list) 1.
 
-Fixpoint env_dom {A} (Γ : env A) : list string :=
+Fixpoint env_dom {A} (Γ : env A) : list ident :=
   match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
 
 Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
@@ -48,28 +46,28 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
      match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
   end.
 
-Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
+Fixpoint env_replace {A} (i: ident) (Γi: env A) (Γ: env A) : option (env A) :=
   match Γ with
   | Enil => None
   | Esnoc Γ j x =>
-     if string_beq i j then env_app Γi Γ else
+     if ident_beq i j then env_app Γi Γ else
      match Γi !! j with
      | None => Γ' ← env_replace i Γi Γ; Some (Esnoc Γ' j x)
      | Some _ => None
      end
   end.
 
-Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
+Fixpoint env_delete {A} (i : ident) (Γ : env A) : env A :=
   match Γ with
   | Enil => Enil
-  | Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
+  | Esnoc Γ j x => if ident_beq i j then Γ else Esnoc (env_delete i Γ) j x
   end.
 
-Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
+Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
   match Γ with
   | Enil => None
   | Esnoc Γ j x =>
-     if string_beq i j then Some (x,Γ)
+     if ident_beq i j then Some (x,Γ)
      else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
   end.
 
@@ -88,15 +86,15 @@ Inductive env_subenv {A} : relation (env A) :=
 Section env.
 Context {A : Type}.
 Implicit Types Γ : env A.
-Implicit Types i : string.
+Implicit Types i : ident.
 Implicit Types x : A.
 Hint Resolve Esnoc_wf Enil_wf.
 
 Ltac simplify :=
   repeat match goal with
   | _ => progress simplify_eq/=
-  | H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2)
-  | |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2)
+  | H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
+  | |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
   | _ => case_match
   end.
 
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index d36317e05e53835f8157b24c214dae57b9531f16..524d6ddae94fb43ad191f1581fb27fb95124d001 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tokens sel_patterns.
 Set Default Proof Using "Type".
 
 Inductive intro_pat :=
-  | IName : string → intro_pat
+  | IIdent : ident → intro_pat
   | IAnom : intro_pat
   | IDrop : intro_pat
   | IFrame : intro_pat
@@ -73,7 +73,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   match ts with
   | [] => Some k
   | TName "_" :: ts => parse_go ts (SPat IDrop :: k)
-  | TName s :: ts => parse_go ts (SPat (IName s) :: k)
+  | TName s :: ts => parse_go ts (SPat (IIdent s) :: k)
   | TAnom :: ts => parse_go ts (SPat IAnom :: k)
   | TFrame :: ts => parse_go ts (SPat IFrame :: k)
   | TBracketL :: ts => parse_go ts (SList :: k)
@@ -98,11 +98,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   end
 with parse_clear (ts : list token) (k : stack) : option stack :=
   match ts with
-  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
+  | TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelIdent s)) :: k)
   | TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
   | TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
   | TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
-  | TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
+  | TName s :: ts => parse_clear ts (SPat (IClear (SelIdent s)) :: k)
   | TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
   | TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
   | TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
@@ -134,6 +134,7 @@ Ltac parse s :=
      lazymatch eval vm_compute in (parse s) with
      | Some ?pats => pats | _ => fail "invalid list intro_pat" s
      end
+  | ident => constr:([IIdent s])
   | ?X => fail "intro_pat.parse:" s "has unexpected type" X
   end.
 Ltac parse_one s :=
@@ -165,6 +166,7 @@ Ltac intro_pat_persistent p :=
   | string =>
      let pat := intro_pat.parse p in
      eval cbv in (forallb intro_pat_persistent pat)
+  | ident => false
   | bool => p
   | ?X => fail "intro_pat_persistent:" p "has unexpected type" X
   end.
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index de56cc823f821fac50da28ee3175834c3604bc66..09722191074d25d98729684cf5380cb7bb6e4ab2 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -8,9 +8,12 @@ Arguments Enil {_}.
 Arguments Esnoc {_} _%proof_scope _%string _%uPred_scope.
 
 Notation "" := Enil (only printing) : proof_scope.
-Notation "Γ H : P" := (Esnoc Γ H P)
+Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
+Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
+  (at level 1, P at level 200,
+   left associativity, format "Γ '_'  :  P '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ) Q%I)
diff --git a/theories/proofmode/sel_patterns.v b/theories/proofmode/sel_patterns.v
index 6fa4129af1736a2e6473014339bb2f716d5f5522..6d7710d6e3aaf5442c9a425abe79681723dd2e01 100644
--- a/theories/proofmode/sel_patterns.v
+++ b/theories/proofmode/sel_patterns.v
@@ -6,7 +6,7 @@ Inductive sel_pat :=
   | SelPure
   | SelPersistent
   | SelSpatial
-  | SelName : string → sel_pat.
+  | SelIdent : ident → sel_pat.
 
 Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
   match ps with
@@ -19,7 +19,7 @@ Module sel_pat.
 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 (SelName s :: k)
+  | TName s :: ts => parse_go ts (SelIdent s :: k)
   | TPure :: ts => parse_go ts (SelPure :: k)
   | TAlways :: ts => parse_go ts (SelPersistent :: k)
   | TSep :: ts => parse_go ts (SelSpatial :: k)
@@ -32,7 +32,9 @@ Ltac parse s :=
   lazymatch type of s with
   | sel_pat => constr:([s])
   | list sel_pat => s
-  | list string => eval vm_compute in (SelName <$> s)
+  | ident => constr:([SelIdent s])
+  | list ident => eval vm_compute in (SelIdent <$> s)
+  | list string => eval vm_compute in (SelIdent ∘ INamed <$> s)
   | string =>
      lazymatch eval vm_compute in (parse s) with
      | Some ?pats => pats | _ => fail "invalid sel_pat" s
diff --git a/theories/proofmode/spec_patterns.v b/theories/proofmode/spec_patterns.v
index 691ba64d586d36fd621abf7b1fa22b1fe374e97a..64201daf270d2f560a1a6356fe8682588c4e990a 100644
--- a/theories/proofmode/spec_patterns.v
+++ b/theories/proofmode/spec_patterns.v
@@ -1,5 +1,5 @@
 From stdpp Require Export strings.
-From iris.proofmode Require Import tokens.
+From iris.proofmode Require Import base tokens.
 Set Default Proof Using "Type".
 
 Inductive goal_kind := GSpatial | GModal | GPersistent.
@@ -7,14 +7,14 @@ Inductive goal_kind := GSpatial | GModal | GPersistent.
 Record spec_goal := SpecGoal {
   spec_goal_kind : goal_kind;
   spec_goal_negate : bool;
-  spec_goal_frame : list string;
-  spec_goal_hyps : list string;
+  spec_goal_frame : list ident;
+  spec_goal_hyps : list ident;
   spec_goal_done : bool
 }.
 
 Inductive spec_pat :=
   | SForall : spec_pat
-  | SName : string → spec_pat
+  | SIdent : ident → spec_pat
   | SPureGoal : bool → spec_pat
   | SGoal : spec_goal → spec_pat
   | SAutoFrame : goal_kind → spec_pat.
@@ -36,7 +36,7 @@ Inductive state :=
 Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | [] => Some (reverse k)
-  | TName s :: ts => parse_go ts (SName s :: k)
+  | TName s :: ts => parse_go ts (SIdent s :: k)
   | TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
      parse_go ts (SAutoFrame GPersistent :: k)
   | TBracketL :: TFrame :: TBracketR :: ts =>
@@ -52,14 +52,14 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
   | _ => None
   end
 with parse_goal (ts : list token)
-    (ki : goal_kind) (neg : bool) (frame hyps : list string)
+    (ki : goal_kind) (neg : bool) (frame hyps : list ident)
     (k : list spec_pat) : option (list spec_pat) :=
   match ts with
   | TMinus :: ts =>
      guard (¬neg ∧ frame = [] ∧ hyps = []);
      parse_goal ts ki true frame hyps k
-  | TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
-  | TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
+  | TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
+  | TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
   | TDone :: TBracketR :: ts =>
      parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
   | TBracketR :: ts =>
@@ -76,11 +76,4 @@ Ltac parse s :=
               | Some ?pats => pats | _ => fail "invalid list spec_pat" s
               end
   end.
-Ltac parse_one s :=
-  lazymatch type of s with
-  | spec_pat => s
-  | string => lazymatch eval vm_compute in (parse s) with
-              | Some [?pat] => pat | _ => fail "invalid spec_pat" s
-              end
-  end.
 End spec_pat.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 40277672d4a238e346fac91e236ce8e8c01349c1..ca5444076c210e36d87f595eb1cc68ca6ad5aa27 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -3,11 +3,12 @@ From iris.proofmode Require Import base intro_patterns spec_patterns sel_pattern
 From iris.base_logic Require Export base_logic big_op.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
-From stdpp Require Import stringmap hlist.
+From stdpp Require Import hlist pretty.
 Set Default Proof Using "Type".
+Export ident.
 
 Declare Reduction env_cbv := cbv [
-  beq ascii_beq string_beq
+  beq ascii_beq string_beq positive_beq ident_beq
   env_lookup env_lookup_delete env_delete env_app env_replace env_dom
   env_persistent env_spatial env_spatial_is_nil envs_dom
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
@@ -20,16 +21,19 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
 
 (** * Misc *)
 (* Tactic Notation tactics cannot return terms *)
-Ltac iFresh' H :=
+Ltac iFresh :=
   lazymatch goal with
   |- envs_entails ?Δ _ =>
      (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
      first use [cbv] to compute the domain of [Δ] *)
      let Hs := eval cbv in (envs_dom Δ) in
-     eval vm_compute in (fresh_string_of_set H (of_list Hs))
-  | _ => H
+     eval vm_compute in
+       (IAnon (match Hs with
+         | [] => 1
+         | _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
+         end))%positive
+  | _ => constr:(IAnon 1)
   end.
-Ltac iFresh := iFresh' "~".
 
 Ltac iMissingHyps Hs :=
   let Δ :=
@@ -83,7 +87,7 @@ Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
 
 Local Inductive esel_pat :=
   | ESelPure
-  | ESelName : bool → string → esel_pat.
+  | ESelIdent : bool → ident → esel_pat.
 
 Ltac iElaborateSelPat pat :=
   let rec go pat Δ Hs :=
@@ -93,14 +97,14 @@ Ltac iElaborateSelPat pat :=
     | SelPersistent :: ?pat =>
        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)
+       go pat Δ' ((ESelIdent true <$> Hs') ++ Hs)
     | 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)
-    | SelName ?H :: ?pat =>
+       go pat Δ' ((ESelIdent false <$> Hs') ++ Hs)
+    | SelIdent ?H :: ?pat =>
        lazymatch eval env_cbv in (envs_lookup_delete H Δ) with
-       | Some (?p,_,?Δ') => go pat Δ' (ESelName p H :: Hs)
+       | Some (?p,_,?Δ') => go pat Δ' (ESelIdent p H :: Hs)
        | None => fail "iElaborateSelPat:" H "not found"
        end
     end in
@@ -109,14 +113,16 @@ Ltac iElaborateSelPat pat :=
     let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
   end.
 
+Local Ltac iClearHyp H :=
+  eapply tac_clear with _ H _ _; (* (i:=H) *)
+    [env_reflexivity || fail "iClear:" H "not found"|].
+
 Tactic Notation "iClear" constr(Hs) :=
   let rec go Hs :=
     lazymatch Hs with
     | [] => idtac
     | ESelPure :: ?Hs => clear; go Hs
-    | ESelName _ ?H :: ?Hs =>
-       eapply tac_clear with _ H _ _; (* (i:=H) *)
-         [env_reflexivity || fail "iClear:" H "not found"|go Hs]
+    | ESelIdent _ ?H :: ?Hs => iClearHyp H; go Hs
     end in
   let Hs := iElaborateSelPat Hs in go Hs.
 
@@ -260,7 +266,7 @@ Tactic Notation "iFrame" constr(Hs) :=
     | SelPure :: ?Hs => iFrameAnyPure; go Hs
     | SelPersistent :: ?Hs => iFrameAnyPersistent; go Hs
     | SelSpatial :: ?Hs => iFrameAnySpatial; go Hs
-    | SelName ?H :: ?Hs => iFrameHyp H; go Hs
+    | SelIdent ?H :: ?Hs => iFrameHyp H; go Hs
     end
   in let Hs := sel_pat.parse Hs in go Hs.
 Tactic Notation "iFrame" "(" constr(t1) ")" constr(Hs) :=
@@ -406,7 +412,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
     | SForall :: ?pats =>
        idtac "the * specialization pattern is deprecated because it is applied implicitly";
        go H1 pats
-    | SName ?H2 :: ?pats =>
+    | SIdent ?H2 :: ?pats =>
        eapply tac_specialize with _ _ H2 _ H1 _ _ _ _; (* (j:=H1) (i:=H2) *)
          [env_reflexivity || fail "iSpecialize:" H2 "not found"
          |env_reflexivity || fail "iSpecialize:" H1 "not found"
@@ -486,12 +492,17 @@ defaults to [false] (i.e. spatial hypotheses are not preserved). *)
 Tactic Notation "iSpecializeCore" open_constr(t) "as" constr(p) :=
   let p := intro_pat_persistent p in
   let t :=
-    match type of t with string => constr:(ITrm t hnil "") | _ => t end in
+    match type of t with
+    | string => constr:(ITrm (INamed t) hnil "")
+    | ident => constr:(ITrm t hnil "")
+    | _ => t
+    end in
   lazymatch t with
   | ITrm ?H ?xs ?pat =>
     let pat := spec_pat.parse pat in
+    let H := lazymatch type of H with string => constr:(INamed H) | _ => H end in
     lazymatch type of H with
-    | string =>
+    | ident =>
       (* The lemma [tac_specialize_persistent_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
@@ -553,8 +564,8 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
     "as" constr(p) constr(lazy_tc) tactic(tac) :=
   try iStartProof;
   let Htmp := iFresh in
-  let t :=
-    lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
+  let t := lazymatch lem with ITrm ?t ?xs ?pat => t | _ => lem end in
+  let t := lazymatch type of t with string => constr:(INamed t) | _ => t end in
   let spec_tac _ :=
     lazymatch lem with
     | ITrm ?t ?xs ?pat => iSpecializeCore (ITrm Htmp xs pat) as p
@@ -562,7 +573,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
     end in
   let go goal_tac :=
     lazymatch type of t with
-    | string =>
+    | ident =>
        eapply tac_pose_proof_hyp with _ _ t _ Htmp _;
          [env_reflexivity || fail "iPoseProof:" t "not found"
          |env_reflexivity || fail "iPoseProof:" Htmp "not fresh"
@@ -618,7 +629,7 @@ Tactic Notation "iRevert" constr(Hs) :=
     | ESelPure :: ?Hs =>
        repeat match goal with x : _ |- _ => revert x end;
        go Hs
-    | ESelName _ ?H :: ?Hs =>
+    | ESelIdent _ ?H :: ?Hs =>
        eapply tac_revert with _ H _ _; (* (i:=H2) *)
          [env_reflexivity || fail "iRevert:" H "not found"
          |env_cbv; go Hs]
@@ -705,6 +716,7 @@ Tactic Notation "iSplit" :=
 Tactic Notation "iSplitL" constr(Hs) :=
   iStartProof;
   let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
   eapply tac_sep_split with _ _ Left Hs _ _; (* (js:=Hs) *)
     [apply _ ||
      let P := match goal with |- FromAnd _ ?P _ _ => P end in
@@ -717,6 +729,7 @@ Tactic Notation "iSplitL" constr(Hs) :=
 Tactic Notation "iSplitR" constr(Hs) :=
   iStartProof;
   let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
   eapply tac_sep_split with _ _ Right Hs _ _; (* (js:=Hs) *)
     [apply _ ||
      let P := match goal with |- FromAnd _ ?P _ _ => P end in
@@ -748,6 +761,7 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
 (** * Combinining hypotheses *)
 Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
   let Hs := words Hs in
+  let Hs := eval vm_compute in (INamed <$> Hs) in
   eapply tac_combine with _ _ Hs _ _ H _;
     [env_reflexivity ||
      let Hs := iMissingHyps Hs in
@@ -844,10 +858,14 @@ Tactic Notation "iModCore" constr(H) :=
 Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
   let rec go Hz pat :=
     lazymatch pat with
-    | IAnom => idtac
-    | IDrop => iClear Hz
-    | IFrame => iFrame Hz
-    | IName ?y => iRename Hz into y
+    | IAnom =>
+       lazymatch Hz with
+       | IAnon _ => idtac
+       | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
+       end
+    | IDrop => iClearHyp Hz
+    | IFrame => iFrameHyp Hz
+    | IIdent ?y => iRename Hz into y
     | IList [[]] => iExFalso; iExact Hz
     | IList [[?pat1; IDrop]] => iAndDestructChoice Hz as Left Hz; go Hz pat1
     | IList [[IDrop; ?pat2]] => iAndDestructChoice Hz as Right Hz; go Hz pat2
@@ -919,9 +937,9 @@ Tactic Notation "iIntros" constr(pat) :=
     | [] => idtac
     (* Optimizations to avoid generating fresh names *)
     | IPureElim :: ?pats => iIntro (?); go pats
-    | IAlwaysElim (IName ?H) :: ?pats => iIntro #H; go pats
+    | IAlwaysElim (IIdent ?H) :: ?pats => iIntro #H; go pats
     | IDrop :: ?pats => iIntro _; go pats
-    | IName ?H :: ?pats => iIntro H; go pats
+    | IIdent ?H :: ?pats => iIntro H; go pats
     (* Introduction patterns that can only occur at the top-level *)
     | IPureIntro :: ?pats => iPureIntro; go pats
     | IAlwaysIntro :: ?pats => iAlways; go pats
@@ -1153,10 +1171,10 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
     lazymatch Hs with
     | [] => tac
     | ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
-    | ESelName ?p ?H :: ?Hs =>
+    | ESelIdent ?p ?H :: ?Hs =>
        iRevert H; go Hs;
        let H' :=
-         match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
+         match p with true => constr:([IAlwaysElim (IIdent H)]) | false => H end in
        iIntros H'
     end in
   try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
@@ -1226,14 +1244,17 @@ Instance copy_destruct_persistently {M} (P : uPred M) :
   CopyDestruct P → CopyDestruct (□ P).
 
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
-  let hyp_name :=
+  let ident :=
     lazymatch type of lem with
-    | string => constr:(Some lem)
+    | ident => constr:(Some lem)
+    | string => constr:(Some (INamed lem))
     | iTrm =>
        lazymatch lem with
-       | @iTrm string ?H _ _ => constr:(Some H) | _ => constr:(@None string)
+       | @iTrm ident ?H _ _ => constr:(Some H)
+       | @iTrm string ?H _ _ => constr:(Some (INamed H))
+       | _ => constr:(@None ident)
        end
-    | _ => constr:(@None string)
+    | _ => constr:(@None ident)
     end in
   let intro_destruct n :=
     let rec go n' :=
@@ -1253,7 +1274,7 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
      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
      (which cannot be kept). *)
-     lazymatch hyp_name with
+     lazymatch ident with
      | None => iPoseProofCore lem as p false tac
      | Some ?H =>
         lazymatch iTypeOf H with
@@ -1357,17 +1378,22 @@ result in the following actions:
 - Introduce the proofmode hypotheses [Hs]
 *)
 Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
-  let rec fix_ihs :=
+  let rec fix_ihs rev_tac :=
     lazymatch goal with
     | H : context [envs_entails _ _] |- _ =>
        eapply (tac_revert_ih _ _ _ H _);
-         [reflexivity
-          || fail "iInduction: spatial context not empty, this should not happen"|];
-       clear H; fix_ihs;
-       let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
-    | _ => idtac
+         [env_reflexivity
+          || fail "iInduction: spatial context not empty, this should not happen"
+         |clear H];
+       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')];
+         let j := eval vm_compute in (1 + j)%N in
+         rev_tac j)
+    | _ => rev_tac 0%N
     end in
-  induction x as pat; fix_ihs.
+  induction x as pat; fix_ihs ltac:(fun _ => idtac).
 
 Ltac iHypsContaining x :=
   let rec go Γ x Hs :=
@@ -1381,7 +1407,7 @@ Ltac iHypsContaining x :=
      end in
   let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
   let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
-  let Hs := go Γp x (@nil string) in go Γs x Hs.
+  let Hs := go Γp x (@nil ident) in go Γs x Hs.
 
 Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
   iRevertIntros Hs with (
@@ -1634,7 +1660,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
        let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
-      |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
+      |intros ??? ->; reflexivity|lazy beta; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) := iRewriteCore Right lem.
 Tactic Notation "iRewrite" "-" open_constr(lem) := iRewriteCore Left lem.
@@ -1649,7 +1675,7 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity
-      |env_reflexivity|lazy beta; iClear Heq]).
+      |env_reflexivity|lazy beta; iClearHyp Heq]).
 
 Tactic Notation "iRewrite" open_constr(lem) "in" constr(H) :=
   iRewriteCore Right lem in H.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 748c1951233ad99fa745bd02b3176a30666f6ebd..b1cd8665d3aafe92c53bf0d5587d09d877d8478b 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -30,7 +30,7 @@ Proof.
   iRight.
   iDestruct "H1" as (z1 z2 c) "(H1&_&#Hc)".
   iPoseProof "Hc" as "foo".
-  iRevert (a b) "Ha Hb". iIntros (b a) "Hb {foo} Ha".
+  iRevert (a b) "Ha Hb". iIntros (b a) "? {foo} Ha".
   iAssert (uPred_ownM (a â‹… core a)) with "[Ha]" as "[Ha #Hac]".
   { by rewrite cmra_core_r. }
   iIntros "{$Hac $Ha}".
@@ -98,7 +98,7 @@ Lemma test_very_fast_iIntros P :
 Proof. by iIntros. Qed.
 
 Lemma test_iDestruct_spatial_and P Q1 Q2 : P ∗ (Q1 ∧ Q2) -∗ P ∗ Q1.
-Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
+Proof. iIntros "[H [? _]]". by iFrame. Qed.
 
 Lemma test_iFrame_pure (x y z : M) :
   ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).
@@ -116,7 +116,7 @@ Qed.
 
 Lemma test_iSpecialize_auto_frame P Q R :
   (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R.
-Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
+Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
 
 (* Check coercions *)
 Lemma test_iExist_coercion (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x.