From 0bcacaa4baabc561add3500fd726a0ddeb31e36a Mon Sep 17 00:00:00 2001
From: Alex Keizer <alex@keizer.dev>
Date: Tue, 8 Oct 2024 20:58:36 -0500
Subject: [PATCH] fix tests

---
 Test/DeadWrap.lean | 4 ++--
 Test/Wrap.lean     | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Test/DeadWrap.lean b/Test/DeadWrap.lean
index 003ce81..4bf8524 100644
--- a/Test/DeadWrap.lean
+++ b/Test/DeadWrap.lean
@@ -8,11 +8,11 @@ namespace Test
 data DeadWrap (α : Type) β
   | mk : α → DeadWrap α β
 
-/-- info: 'Test.DeadWrap.Base' does not depend on any axioms  -/
+/-- info: 'Test.DeadWrap.Base' depends on axioms: [propext, Quot.sound] -/
 #guard_msgs in
   #print axioms DeadWrap.Base
 
-/-- info: Test.DeadWrap.mk {α β : Type} (a✝ : α) : DeadWrap α β -/
+/-- info: Test.DeadWrap.mk {α β : Type} : α → DeadWrap α β -/
 #guard_msgs in
   #check DeadWrap.mk
 
diff --git a/Test/Wrap.lean b/Test/Wrap.lean
index 652ff03..0840ad4 100644
--- a/Test/Wrap.lean
+++ b/Test/Wrap.lean
@@ -7,7 +7,7 @@ namespace Test
 data Wrap α
   | mk : α → Wrap α
 
-/-- info: Test.Wrap.mk {α : Type} (a✝ : α) : Wrap α -/
+/-- info: Test.Wrap.mk {α : Type} : α → Wrap α -/
 #guard_msgs in
   #check Wrap.mk