From c1fccf19cb8f15daba2329e5c82c6feca825c02b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Jan 2022 11:46:11 -0800
Subject: [PATCH] chore: fix test

---
 tests/compiler/foreign/Main/S.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/compiler/foreign/Main/S.lean b/tests/compiler/foreign/Main/S.lean
index a5ff00cdcb..3af72fa8e4 100644
--- a/tests/compiler/foreign/Main/S.lean
+++ b/tests/compiler/foreign/Main/S.lean
@@ -1,4 +1,4 @@
-constant SPointed : PointedType
+constant SPointed : NonemptyType
 def S : Type := SPointed.type
 instance : Nonempty S := SPointed.property