From 358a129d78ea76cbbd58a7e904d2b96ba130890d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Fri, 6 Aug 2021 17:21:46 -0400
Subject: [PATCH] fix: protect `rfl`

---
 src/Init/Core.lean    | 2 +-
 src/Init/Prelude.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index e9e8779135..b4f78e6b80 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -284,7 +284,7 @@ theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (
 theorem Iff.refl (a : Prop) : a ↔ a :=
   Iff.intro (fun h => h) (fun h => h)
 
-theorem Iff.rfl {a : Prop} : a ↔ a :=
+protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index c26993f12f..383e5c6e07 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -107,7 +107,7 @@ init_quot
 inductive HEq {α : Sort u} (a : α) : {β : Sort u} → β → Prop where
   | refl {} : HEq a a
 
-@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
+@[matchPattern] protected def HEq.rfl {α : Sort u} {a : α} : HEq a a :=
   HEq.refl a
 
 theorem eq_of_heq {α : Sort u} {a a' : α} (h : HEq a a') : Eq a a' :=