aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqwc.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqwc.mll')
-rw-r--r--tools/coqwc.mll1
1 files changed, 0 insertions, 1 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index a5376ec44..50f989e7c 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -15,7 +15,6 @@
(*i*){
open Printf
open Lexing
-open Filename
(*i*)
(*s Command-line options. *)