summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/HoTT_coq_053.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_053.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_053.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
index a14fb6aa..e2bf1dbe 100644
--- a/test-suite/bugs/closed/HoTT_coq_053.v
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -39,7 +39,7 @@ Definition NatCategory (n : nat) :=
Definition NatCategory' (n : nat) :=
match n with
| 0 => (fun X => @Build_PreCategory X
- (fun _ _ => Unit : Prop)) Unit
+ (fun _ _ => Unit : Set)) Unit
| _ => DiscreteCategory Bool
end.