summaryrefslogtreecommitdiff
path: root/compiler/Extract.ml
diff options
context:
space:
mode:
authorSon Ho2023-09-07 16:02:43 +0200
committerSon Ho2023-09-07 16:02:43 +0200
commit1181aecddbcb3232c21b191fbde59c2e9596846a (patch)
treed246e01bb874f44ae6e10164ee357f1fbb6caf11 /compiler/Extract.ml
parent8b18c0da053e069b5a2d9fbf06f45eae2f05a029 (diff)
Fix some issues
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 74540787..8baa3c88 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -8,7 +8,6 @@ open Pure
open PureUtils
open TranslateCore
open ExtractBase
-open ExtractAssumed
open StringUtils
open Config
module F = Format