diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 1e76c78fe609e1a8682b55c9e70a72fc249c33d5..aadc9a54f6e0661775b4a5bbb23efe4e14d7e227 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 
 Inductive intro_pat :=
   | IIdent : ident → intro_pat
-  | IAnom : intro_pat
+  | IFresh : intro_pat
   | IDrop : intro_pat
   | IFrame : intro_pat
   | IList : list (list intro_pat) → intro_pat
@@ -74,7 +74,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | [] => Some k
   | TName "_" :: ts => parse_go ts (StPat IDrop :: k)
   | TName s :: ts => parse_go ts (StPat (IIdent s) :: k)
-  | TAnom :: ts => parse_go ts (StPat IAnom :: k)
+  | TAnon :: ts => parse_go ts (StPat IFresh :: k)
   | TFrame :: ts => parse_go ts (StPat IFrame :: k)
   | TBracketL :: ts => parse_go ts (StList :: k)
   | TBar :: ts => parse_go ts (StBar :: k)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 52b46c8302e631a6e833c1071d41157ead18075d..30c42ee1f0c9ac9ac0589b9dd3c41a489c04f6c8 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1219,7 +1219,7 @@ Tactic Notation "iModCore" constr(H) :=
 (** * Basic destruct tactic *)
 Local Ltac iDestructHypGo Hz pat :=
   lazymatch pat with
-  | IAnom =>
+  | IFresh =>
      lazymatch Hz with
      | IAnon _ => idtac
      | INamed ?Hz => let Hz' := iFresh in iRename Hz into Hz'
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index 47e04bec35747fe904bf5da01c2687ce41aecdee..ed3a8b8f8824fef0b09896b24abfb57416dd41fc 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 Inductive token :=
   | TName : string → token
   | TNat : nat → token
-  | TAnom : token
+  | TAnon : token
   | TFrame : token
   | TBar : token
   | TBracketL : token
@@ -43,7 +43,7 @@ Definition cons_state (kn : state) (k : list token) : list token :=
 Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   match s with
   | "" => reverse (cons_state kn k)
-  | String "?" s => tokenize_go s (TAnom :: cons_state kn k) SNone
+  | String "?" s => tokenize_go s (TAnon :: cons_state kn k) SNone
   | String "$" s => tokenize_go s (TFrame :: cons_state kn k) SNone
   | String "[" s => tokenize_go s (TBracketL :: cons_state kn k) SNone
   | String "]" s => tokenize_go s (TBracketR :: cons_state kn k) SNone