diff --git "a/theories/\316\275Type/HSet.v" "b/theories/\316\275Type/HSet.v"
index feaea22..3f7ab78 100644
--- "a/theories/\316\275Type/HSet.v"
+++ "b/theories/\316\275Type/HSet.v"
@@ -7,6 +7,8 @@ From Bonak Require Import Notation.
 Set Primitive Projections.
 Set Universe Polymorphism.
 
+Set Primitive Projections.
+
 Record HSet := {
   Dom:> Type;
   UIP {x y: Dom} {h g: x = y}: h = g;