Skip to content

Commit a99c6c3

Browse files
jdchristensenjdchristensen
committed
test/WildCat/AbEnriched: add "From HoTT" to imports to fix opam build
1 parent 5ac04a3 commit a99c6c3

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

‎test/WildCat/AbEnriched.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1-
Require Import WildCat.SetoidRewrite WildCat.Core WildCat.AbEnriched.
2-
Require Import Basics.Overture.
1+
From HoTT Require Import WildCat.SetoidRewrite WildCat.Core WildCat.AbEnriched.
2+
From HoTT Require Import Basics.Overture.
33

44
Local Open Scope mc_add_scope.
55

0 commit comments

Comments
 (0)