aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 04182cf23..c6f49dcd4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -9,7 +9,6 @@
open Pp
open Errors
open Util
-open System
open Flags
open Names
open Libnames