diff --git a/test/bugs/github754.v b/test/bugs/github754.v index 11df5b43e39..be6f19f3d3c 100644 --- 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.