Primitive Projections in HSet.v

artagnon · Feb 19, 2024 · 9685d4a · 9685d4a
1 parent f5f42f9
commit 9685d4a
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/νType/HSet.v b/theories/νType/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;