From c98c721b5c2ad43832e63dca7c01234a7fa41ecc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 29 Apr 2019 21:36:03 +0200
Subject: [PATCH] Rename misspelled `IAnom` into `IFresh` (`IAnon` is already
 in use).

---
 theories/proofmode/intro_patterns.v | 4 ++--
 theories/proofmode/ltac_tactics.v   | 2 +-
 theories/proofmode/tokens.v         | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 1e76c78fe..aadc9a54f 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 52b46c830..30c42ee1f 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 47e04bec3..ed3a8b8f8 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
-- 
GitLab