From 87913c4014f01a23d608457e379b74aa1befd4ab Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 27 Dec 2021 17:21:32 +0000
Subject: Introduce Everything.agda to aid in overall compilation.

---
 src/Helium/Semantics/Denotational/Core.agda | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'src/Helium/Semantics/Denotational')

diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 54f0375..359fbd4 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -1,6 +1,10 @@
-{-# OPTIONS --safe --without-K #-}
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for the denotational semantics.
+------------------------------------------------------------------------
 
-open import Helium.Data.Pseudocode
+{-# OPTIONS --safe --without-K #-}
 
 module Helium.Semantics.Denotational.Core
   {ℓ′}
-- 
cgit v1.2.3