summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGabriel Kerneis2013-11-11 10:22:47 +0000
committerGabriel Kerneis2013-11-11 10:22:47 +0000
commit2c7bf65b9c256a0d9bc3e4a5dfdeb3c208da2d61 (patch)
treedca946e8b4a477d0eedf4f2a99f7d0fa329f832f /src
parentf0bbc49b54862bec08df26fa753ac270f2042ae4 (diff)
Remove workaround for a bug fixed in Lem
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/interp.lem1
-rw-r--r--src/lem_interp/interp_lib.lem1
2 files changed, 0 insertions, 2 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a9f747da..2e8af9d3 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -2,7 +2,6 @@ open import Pervasives
import Map
import Map_extra
import Maybe
-open import List (* because bug inline lookup/lookupBy *)
import List_extra
open import Interp_ast
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 546cf143..192cd641 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -1,6 +1,5 @@
open import Interp ;;
import Maybe_extra
-open import List
let add v = v ;;