From d9ca2751c2f05e32ea9db8f3954c4fa4346554d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Feb 2020 11:43:14 -0800
Subject: [PATCH] chore: mark `MutQuot.val` as `[neverExtract]`

---
 src/Init/MutQuot.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/MutQuot.lean b/src/Init/MutQuot.lean
index 9b87995abf..4fe5cbca54 100644
--- a/src/Init/MutQuot.lean
+++ b/src/Init/MutQuot.lean
@@ -12,7 +12,7 @@ structure MutQuot {α : Type u} (r : α → α → Prop) :=
 mkAux :: (val : Quot r)
 
 attribute [extern "lean_mutquot_mk"] MutQuot.mkAux
-attribute [extern "lean_mutquot_get"] MutQuot.val
+attribute [extern "lean_mutquot_get", neverExtract] MutQuot.val
 
 @[extern "lean_mutquot_mk"]
 def MutQuot.mk {α : Type u} (r : α → α → Prop) (a : α) : MutQuot r :=