Don't reexport Vote (the type) from TransactionStructure

IntersectMBO · Oct 20, 2023 · 4a6b1de · 4a6b1de
1 parent 4443ea5
commit 4a6b1de
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 6 deletions.
diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda
@@ -173,7 +173,7 @@ HSGovStructure = record
   }
 instance _ = HSGovStructure
 
-open import Ledger.GovernanceActions it
+open import Ledger.GovernanceActions it hiding (Vote)
 open import Ledger.Deleg it
 open import Ledger.Gov it
 
@@ -262,8 +262,8 @@ instance
 
   Convertible-Tag : Convertible Tag F.Tag
   Convertible-Tag = λ where
-    .to   → λ{ Spend → Spend; Mint → Mint; Cert → Cert; Rewrd → Rewrd; Vote → F.Vote; Propose → Propose }
-    .from → λ{ Spend → Spend; Mint → Mint; Cert → Cert; Rewrd → Rewrd; Vote → Tag.Vote; Propose → Propose }
+    .to   → λ{ Spend → Spend; Mint → Mint; Cert → Cert; Rewrd → Rewrd; Vote → Vote; Propose → Propose }
+    .from → λ{ Spend → Spend; Mint → Mint; Cert → Cert; Rewrd → Rewrd; Vote → Vote; Propose → Propose }
    where open F.Tag
 
   Convertible-TxWitnesses : Convertible TxWitnesses F.TxWitnesses

diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda
@@ -89,6 +89,7 @@ open import Ledger.Transaction hiding (Vote)
 
 module Ledger.Ratify (txs : _) (open TransactionStructure txs) where
 
+open import Ledger.GovernanceActions govStructure using (Vote)
 open import Ledger.Gov govStructure
 
 infixr 2 _∧_

diff --git a/src/Ledger/ScriptValidation.agda b/src/Ledger/ScriptValidation.agda
@@ -16,7 +16,7 @@ open import Ledger.Crypto
 
 
 module Ledger.ScriptValidation
-  (txs : _) (open TransactionStructure txs hiding (Vote))
+  (txs : _) (open TransactionStructure txs)
   (abs : AbstractFunctions txs) (open AbstractFunctions abs) (open indexOf indexOfImp)
   where
 

diff --git a/src/Ledger/Transaction.lagda b/src/Ledger/Transaction.lagda
@@ -96,7 +96,7 @@ the transaction body are:
     ; govParams = govParams
     }
 
-  open Ledger.GovernanceActions govStructure hiding (yes; no) public
+  open Ledger.GovernanceActions govStructure hiding (Vote; yes; no; abstain) public
   open Ledger.Deleg             govStructure public
 \end{code}
 \emph{Derived types}

diff --git a/src/Ledger/Utxow.lagda b/src/Ledger/Utxow.lagda
@@ -8,7 +8,7 @@ open import Ledger.Abstract
 open import Ledger.Transaction
 
 module Ledger.Utxow
-  (txs : _) (open TransactionStructure txs hiding (Vote))
+  (txs : _) (open TransactionStructure txs)
   (abs : AbstractFunctions txs) (open AbstractFunctions abs)
   where
 open import Ledger.Utxo txs abs