From: Anders Mörtberg <mortberg@chalmers.se>
Date: Wed, 1 Jul 2015 12:38:45 +0000 (+0200)
Subject: Fix imports
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=19ed1a3e02b929f33f208c2e1650e8859a0a5a42;p=cubicaltt.git

Fix imports
---

diff --git a/examples/bool.ctt b/examples/bool.ctt
index fea7111..5688ea7 100644
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -1,6 +1,6 @@
 module bool where
 
-import gradLemma
+import prelude
 
 data bool = false | true
 
diff --git a/examples/int.ctt b/examples/int.ctt
index 46f14ce..16e8e5e 100644
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -2,7 +2,6 @@ module int where
 
 import nat
 import discor
-import gradLemma
 
        ---------------------------------------------------
        -- Example: Non-trivial equality between Z and Z --
diff --git a/examples/pi.ctt b/examples/pi.ctt
index ef82c8c..2f1369b 100644
--- a/examples/pi.ctt
+++ b/examples/pi.ctt
@@ -1,6 +1,6 @@
 module pi where
 
-import gradLemma
+import prelude
 
               -----------------------------------
               -- Example: Equality in pi types --