From 9038d2e886437d8f107709e4db34a245bf1afff6 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 19 Sep 2023 10:40:27 +0200
Subject: [PATCH] chore: disambiguate `whnf` system category

---
 src/kernel/type_checker.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index b09b53557e..ded2680ef1 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -409,7 +409,7 @@ static bool is_let_fvar(local_ctx const & lctx, expr const & e) {
     If `cheap == true`, then we don't perform delta-reduction when reducing major premise of recursors and projections.
     We also do not cache results. */
 expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
-    check_system("whnf");
+    check_system("type checker: whnf");
 
     // handle easy cases
     switch (e.kind()) {