diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 89bc31d0a..1c8d60251 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -12,7 +12,6 @@ open Pp open Errors open Util open Flags -open System open Vernacexpr (* The functions in this module may raise (unexplainable!) exceptions. |