From df85fee62c1f7e8721d712f5aac4a8b095856534 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 1 Aug 2022 06:51:50 -0400
Subject: [PATCH] chore: rename ac_refl to ac_rfl

---
 doc/highlight.js                             |  2 +-
 src/Init/Tactics.lean                        |  2 +-
 src/Lean/Meta/Tactic/AC/Main.lean            |  2 +-
 tests/lean/run/{ac_refl.lean => ac_rfl.lean} | 20 ++++++++++----------
 4 files changed, 13 insertions(+), 13 deletions(-)
 rename tests/lean/run/{ac_refl.lean => ac_rfl.lean} (91%)

diff --git a/doc/highlight.js b/doc/highlight.js
index 175c05d1e7..a9a31fa880 100644
--- a/doc/highlight.js
+++ b/doc/highlight.js
@@ -1123,7 +1123,7 @@ hljs.registerLanguage("lean", function(hljs) {
       'Type Prop|10 Sort rw|10 rewrite rwa erw subst substs ' +
       'simp dsimp simpa simp_intros finish using generalizing ' +
       'unfold unfold1 dunfold unfold_projs unfold_coes ' +
-      'delta cc ac_reflexivity ac_refl ' +
+      'delta cc ac_rfl ' +
       'existsi|10 cases rcases intro intros introv by_cases ' +
       'refl rfl funext case focus propext exact exacts ' +
       'refine apply eapply fapply apply_with apply_instance ' +
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index aa760bfe04..79915c7260 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -169,7 +169,7 @@ macro "rfl" : tactic => `(eq_refl)
   theorems included (relevant for declarations defined by well-founded recursion). -/
 macro "rfl'" : tactic => `(set_option smartUnfolding false in with_unfolding_all rfl)
 
-syntax (name := ac_refl) "ac_refl " : tactic
+syntax (name := acRfl) "ac_rfl" : tactic
 
 /-- `admit` is a shorthand for `exact sorry`. -/
 macro "admit" : tactic => `(exact @sorryAx _ false)
diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean
index 7bc1972097..912d0130da 100644
--- a/src/Lean/Meta/Tactic/AC/Main.lean
+++ b/src/Lean/Meta/Tactic/AC/Main.lean
@@ -168,7 +168,7 @@ where
       | none => return Simp.Step.done { expr := e }
     | e, _ => return Simp.Step.done { expr := e }
 
-@[builtinTactic ac_refl] def ac_refl_tactic : Lean.Elab.Tactic.Tactic := fun _ => do
+@[builtinTactic acRfl] def acRflTactic : Lean.Elab.Tactic.Tactic := fun _ => do
   let goal ← getMainGoal
   rewriteUnnormalized goal
 
diff --git a/tests/lean/run/ac_refl.lean b/tests/lean/run/ac_rfl.lean
similarity index 91%
rename from tests/lean/run/ac_refl.lean
rename to tests/lean/run/ac_rfl.lean
index 11ad669e09..d7e2df4677 100644
--- a/tests/lean/run/ac_refl.lean
+++ b/tests/lean/run/ac_rfl.lean
@@ -49,20 +49,20 @@ instance : IsIdempotent Or := ⟨λ p => propext ⟨λ hp => hp.elim id id, Or.i
 instance : IsNeutral Or False :=
   ⟨λ p => propext ⟨λ hfp => hfp.elim False.elim id, Or.inr⟩, λ p => propext ⟨λ hpf => hpf.elim id False.elim, Or.inl⟩⟩
 
-example (x y z : Nat) : x + y + 0 + z = z + (x + y) := by ac_refl
+example (x y z : Nat) : x + y + 0 + z = z + (x + y) := by ac_rfl
 
-example (x y z : Nat) : (x + y) * (0 + z) = (x + y) * z:= by ac_refl
+example (x y z : Nat) : (x + y) * (0 + z) = (x + y) * z:= by ac_rfl
 
-example (x y z : Nat) : (x + y) * (0 + z) = 1 * z * (y + 0 + x) := by ac_refl
+example (x y z : Nat) : (x + y) * (0 + z) = 1 * z * (y + 0 + x) := by ac_rfl
 
-theorem ex₁ (x y z : Nat) : max (0 + (max x (max z (max (0 + 0) ((max 1 0) + 0 + 0) * y)))) y = max (max x y) z := by ac_refl
+theorem ex₁ (x y z : Nat) : max (0 + (max x (max z (max (0 + 0) ((max 1 0) + 0 + 0) * y)))) y = max (max x y) z := by ac_rfl
 #print ex₁
 
-example (x y : Nat) : 1 + 0 + 0 = 0 + 1 := by ac_refl
+example (x y : Nat) : 1 + 0 + 0 = 0 + 1 := by ac_rfl
 
-example (x y : Nat) : (x + y = 42) = (y + x = 42) := by ac_refl
+example (x y : Nat) : (x + y = 42) = (y + x = 42) := by ac_rfl
 
-example (x y : Nat) (P : Prop) : (x + y = 42 → P) = (y + x = 42 → P) := by ac_refl
+example (x y : Nat) (P : Prop) : (x + y = 42 → P) = (y + x = 42 → P) := by ac_rfl
 
 inductive Vector (α : Type u) : Nat → Type u where
   | nil  : Vector α 0
@@ -72,13 +72,13 @@ def f (n : Nat) (xs : Vector α n) := xs
 
 -- Repro: Dependent types trigger incorrect proofs
 theorem ex₂ (n m : Nat) (xs : Vector α (n+m)) (ys : Vector α (m+n)) : (f (n+m) xs, f (m+n) ys, n+m) = (f (n+m) xs, f (m+n) ys, m+n) := by
-  ac_refl
+  ac_rfl
 
 -- Repro: Binders also trigger invalid proofs
 theorem ex₃ (n : Nat) : (fun x => n + x) = (fun x => x + n) := by
-  ac_refl
+  ac_rfl
 #print ex₃
 
 -- Repro: the Prop universe doesn't work
 example (p q : Prop) : (p ∨ p ∨ q ∧ True) = (q ∨ p) := by
-  ac_refl
+  ac_rfl