From da61adaabced6ab2b1358c709fe4b425582ad138 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 16 Oct 2026 16:48:18 +0200 Subject: [PATCH] Adapt to rocq-prover/rocq#22173 (Delay q <= Type using above_prop) --- test-suite/output/bug_13942.out | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test-suite/output/bug_13942.out b/test-suite/output/bug_13942.out index b6bb3a0c6e..9de7a83c0c 100644 --- a/test-suite/output/bug_13942.out +++ b/test-suite/output/bug_13942.out @@ -4,7 +4,7 @@ The following term contains unresolved implicit arguments: (fi fu) More precisely: - ?A: Cannot infer the implicit parameter A of fi whose type is - "Type" in + "Univ" in environment: K : Type M : Type -> Type @@ -58,7 +58,7 @@ The following term contains unresolved implicit arguments: (fi fu) More precisely: - ?A: Cannot infer the implicit parameter A of fi whose type is - "Type" in + "Univ" in environment: K : Type M : Type -> Type