diff options
Diffstat (limited to 'contrib/interface/blast.ml')
| -rwxr-xr-x | contrib/interface/blast.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 4c57760de..d5715fd3d 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -4,7 +4,6 @@ open Ctast;; open Termops;; open Nameops;; -open Astterm;; open Auto;; open Clenv;; open Command;; |