diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 0946b26437dd475111f73977aa87af996e546f46..aa47143c677ecb0b97e1bdd393d2155a34ff895e 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -36,11 +36,11 @@ Ltac call to "done" failed.
 No applicable tactic.
 The command has indeed failed with message:
 In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"iElaborateSelPat_go", last call failed.
+"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
 In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
-"iElaborateSelPat_go", last call failed.
+"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
 In nested Ltac calls to "iSpecialize (open_constr)",
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 094d74b2d12be4271a5f743237d4dd78299a3e8f..4d5015b3c69753ce3b8937613195235cb450bbfd 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -140,7 +140,7 @@ Local Inductive esel_pat :=
   | ESelPure
   | ESelIdent : bool → ident → esel_pat.
 
-Ltac iElaborateSelPat_go pat Δ Hs :=
+Local Ltac iElaborateSelPat_go pat Δ Hs :=
   lazymatch pat with
   | [] => eval cbv in Hs
   | SelPure :: ?pat =>  iElaborateSelPat_go pat Δ (ESelPure :: Hs)