Use genErrors whenever possible

Author: javierdiaz72

docs/agda-spec/src/Spec/ChainHead/Properties.agda

@@ -19,6 +19,7 @@ module Spec.ChainHead.Properties
   (rs     : _) (open RationalExtStructure rs)
   where
 
+open import Tactic.GenError
 open import Ledger.Prelude
 open import Ledger.PParams crypto es ss using (PParams; ProtVer)
 open import Spec.TickForecast crypto es ss li
@@ -75,7 +76,7 @@ instance
 
       computeProof : ComputationResult String (∃[ s′ ] nes ⊢ s ⇀⦇ bh ,CHAINHEAD⦈ s′)
       computeProof = case ¿ prtlSeqChecks ¿² lab bh of λ where
-        (no _)    → failure "Failed in CHAINHEAD"
+        (no ¬psc) → failure (genErrors ¬psc)
         (yes psc) → do
           (forecast , tickfStep) ← computeTICKF _ nes slot
           let
@@ -84,7 +85,7 @@ instance
             pp = getPParams forecast; open PParams
             pd = getPoolDistr forecast
           case chainChecks? MaxMajorPV (pp .maxHeaderSize , pp .maxBlockSize , pp .pv) bh of λ where
-            (no _)   → failure "Failed in CHAINHEAD"
+            (no ¬cc) → failure (genErrors ¬cc)
             (yes cc) → do
               (⟦ η₀′ , _ ⟧ᵗˢ , ticknStep) ← computeTICKN ticknΓ ticknSt ne
               (_             , prtclStep) ← computePRTCL ⟦ pd , η₀′ ⟧ᵖᵉ prtclSt bh

docs/agda-spec/src/Spec/Protocol/Properties.agda

@@ -19,6 +19,7 @@ module Spec.Protocol.Properties
 
 open import Data.Rational as ℚ using (1ℚ)
 open import Ledger.Prelude
+open import Tactic.GenError
 open import Spec.Protocol crypto nonces es ss bs af rs
 open import Spec.BaseTypes crypto using (OCertCounters)
 open import Spec.UpdateNonce crypto nonces es
@@ -88,7 +89,7 @@ instance
           (_ , updnStep)  ← computeUPDN updnΓ updnSt slot
           (_ , ocertStep) ← computeOCERT ocertΓ cs bh
           success (-, Evolve-Prtcl (updnStep , ocertStep , prf))
-        (no _) → failure "Failed in PRTCL"
+        (no ¬prf) → failure (genErrors ¬prf)
 
       completeness : ∀ s′ → Γ ⊢ s ⇀⦇ bh ,PRTCL⦈ s′ → (proj₁ <$> computeProof) ≡ success s′
       completeness _ (Evolve-Prtcl (updnStep , ocertStep , p))