diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index da335306d..36dfc79cb 100644 --- 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 index 8d2323734..97591752f 100644 --- 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 index 7c5d19a2c..8569491b9 100644 --- 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 index 126451a02..d0502728b 100644 --- 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 index e3774f3e9..fd41f3f54 100644 --- 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