chore: remove old notation

src/Init/Control/ExceptCps.lean

@@ -29,7 +29,7 @@ instance : Monad (ExceptCpsT ε m) where
   bind x f := fun _ k₁ k₂ => x _ (fun a => f a _ k₁ k₂) k₂
 
 instance : LawfulMonad (ExceptCpsT σ m) := by
-  refine! { .. } <;> intros <;> rfl
+  refine' { .. } <;> intros <;> rfl
 
 instance : MonadExceptOf ε (ExceptCpsT ε m) where
   throw e  := fun _ _ k => k e

src/Init/Control/Lawful.lean

@@ -102,7 +102,7 @@ namespace Id
 @[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
 
 instance : LawfulMonad Id := by
-  refine! { .. } <;> intros <;> rfl
+  refine' { .. } <;> intros <;> rfl
 
 end Id
 

src/Init/Control/StateCps.lean

@@ -29,7 +29,7 @@ instance : Monad (StateCpsT σ m) where
   bind x f := fun δ s k => x δ s fun a s => f a δ s k
 
 instance : LawfulMonad (StateCpsT σ m) := by
-  refine! { .. } <;> intros <;> rfl
+  refine' { .. } <;> intros <;> rfl
 
 instance : MonadStateOf σ (StateCpsT σ m) where
   get   := fun δ s k => k s s

src/Init/Notation.lean

@@ -28,7 +28,6 @@ macro "min1" : prec => `(11)   -- `(min+1) we can only `min+1` after `Meta.lean`
 /-
   `max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`.
   We use `max_prec` to workaround bootstrapping issues. -/
-macro "maxPrec!" : term => `(1024)
 macro "max_prec" : term => `(1024)
 
 macro "default" : prio => `(1000)
@@ -198,7 +197,6 @@ syntax (name := contradiction) "contradiction" : tactic
 syntax (name := apply) "apply " term : tactic
 syntax (name := exact) "exact " term : tactic
 syntax (name := refine) "refine " term : tactic
-syntax (name := refine!) "refine! " term : tactic
 syntax (name := refine') "refine' " term : tactic
 syntax (name := case) "case " ident " => " tacticSeq : tactic
 syntax (name := allGoals) "allGoals " tacticSeq : tactic

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -73,11 +73,6 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
   | `(tactic| refine $e) => refineCore e `refine (allowNaturalHoles := false)
   | _                    => throwUnsupportedSyntax
 
-@[builtinTactic «refine!»] def evalRefineBang : Tactic := fun stx =>
-  match stx with
-  | `(tactic| refine! $e) => refineCore e `refine (allowNaturalHoles := true)
-  | _                     => throwUnsupportedSyntax
-
 @[builtinTactic «refine'»] def evalRefine' : Tactic := fun stx =>
   match stx with
   | `(tactic| refine' $e) => refineCore e `refine' (allowNaturalHoles := true)