Merge pull request #2104 from jdchristensen/DProp-test

github754: make this test work again
HoTT · Sep 30, 2024 · 180aa20 · 180aa20
2 parents 63a47b4 + 13a9188
commit 180aa20
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.