From 60f04c1d26b128016e42b8f9a70bec7716f3e227 Mon Sep 17 00:00:00 2001
From: Christian Doczkal <christian.doczkal@inria.fr>
Date: Fri, 18 Jun 2021 12:54:28 +0200
Subject: [PATCH] non-forgetful attribute for pttdom_elabel

---
 theories/pttdom.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/pttdom.v b/theories/pttdom.v
index 7739e8c..315fa6d 100644
--- a/theories/pttdom.v
+++ b/theories/pttdom.v
@@ -205,6 +205,7 @@ Section derived.
  Lemma eqv11 x y z: eqv' x y -> eqv' y z -> x ≡ z.
  Proof. move=> /= -> ->. apply cnvI. Qed.
 
+ #[non_forgetful_inheritance]
  HB.instance Definition pttdom_elabel := 
    Elabel_of_Setoid.Build X eqv'_sym eqv01 eqv11.