From 74ebe48d6ac265b85724b65e44bc9ba2863478ce Mon Sep 17 00:00:00 2001
From: Chandradeep Dey <codesigning@chandradeepdey.com>
Date: Fri, 31 Jul 2026 12:41:34 -0400
Subject: [PATCH] =?UTF-8?q?public.v:=20Remove=20unused=20savedPropG=20?=
 =?UTF-8?q?=CE=A3?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 cryptis/core/public.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/cryptis/core/public.v b/cryptis/core/public.v
index 1cd8d36..0e87d1e 100644
--- a/cryptis/core/public.v
+++ b/cryptis/core/public.v
@@ -16,13 +16,11 @@ Unset Printing Implicit Defensive.
 Class publicGpreS Σ := PublicGPreS {
   publicGpreS_nonce : savedPredG Σ term;
   publicGpreS_seal  : savedPredG Σ (term * term);
-  publicGpreS_prop  : savedPropG Σ;
   publicGpreS_meta  : metaGS Σ;
 }.
 
 Local Existing Instance publicGpreS_nonce.
 Local Existing Instance publicGpreS_seal.
-Local Existing Instance publicGpreS_prop.
 Local Existing Instance publicGpreS_meta.
 
 Class publicGS Σ := PublicGS {
@@ -38,7 +36,6 @@ Global Existing Instance public_inG.
 Definition publicΣ : gFunctors :=
   #[savedPredΣ term;
     savedPredΣ (term * term);
-    savedPropΣ;
     metaΣ].
 
 Global Instance subG_publicGpreS Σ : subG publicΣ Σ → publicGpreS Σ.