From 9685d4ac350ae65d3a4323eff9d1a7fc40a6e98b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 19 Feb 2024 11:12:29 +0100
Subject: [PATCH] Primitive Projections in HSet.v

---
 "theories/\316\275Type/HSet.v" | 2 ++
 1 file changed, 2 insertions(+)

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;