fix

Std.lean

@@ -92,7 +92,6 @@ import Std.Tactic.OpenPrivate
 import Std.Tactic.PermuteGoals
 import Std.Tactic.PrintDependents
 import Std.Tactic.PrintPrefix
-import Std.Tactic.Relation.Rfl
 import Std.Tactic.SeqFocus
 import Std.Tactic.SqueezeScope
 import Std.Tactic.Unreachable

Std/Data/List/Perm.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 -/
 import Std.Tactic.Alias
-import Std.Tactic.Relation.Rfl
 import Std.Data.List.Init.Attach
 import Std.Data.List.Pairwise
+-- Adaptation note: nightly-2024-03-18. We should be able to remove this after nightly-2024-03-19.
+import Lean.Elab.Tactic.Rfl
 
 /-!
 # List Permutations

Std/Logic.lean

@@ -32,9 +32,6 @@ end Classical
 
 theorem heq_iff_eq : HEq a b ↔ a = b := ⟨eq_of_heq, heq_of_eq⟩
 
-theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
-  cases propext (iff_of_true hp hq); rfl
-
 @[simp] theorem eq_rec_constant {α : Sort _} {a a' : α} {β : Sort _} (y : β) (h : a = a') :
     (@Eq.rec α a (fun α _ => β) y a' h) = y := by cases h; rfl
 

test/rfl.lean

@@ -1,4 +1,5 @@
-import Std.Tactic.Relation.Rfl
+import Lean.Elab.Tactic.Rfl
+-- Adaptation note: we should be able to remove this import after nightly-2024-03-19
 
 set_option linter.missingDocs false