github754: make this test work again

HoTT · Sep 30, 2024 · 13a9188 · 13a9188
1 parent 63a47b4
commit 13a9188
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/bugs/github754.v b/test/bugs/github754.v
@@ -1,4 +1,4 @@
-From HoTT Require Import Basics Types DProp Tactics.EquivalenceInduction.
+From HoTT Require Import Basics Types Universes.DProp Tactics.EquivalenceInduction.
 
 Local Open Scope nat_scope.