Silence some compiler warning by avoiding useless opening modules.

5df5ef47 · Guillaume Melquiond · e09ec78a · 5df5ef47 · 5df5ef47 · 5df5ef47
Commit 5df5ef47 authored Dec 03, 2013 by Guillaume Melquiond
13 changed files
--- a/src/core/decl.mli
+++ b/src/core/decl.mli
@@ -9,8 +9,6 @@
 (*                                                                  *)
 (********************************************************************)

-open Stdlib
-
 (** Logic Declarations *)

 open Ident

--- a/src/core/ident.mli
+++ b/src/core/ident.mli
@@ -9,8 +9,6 @@
 (*                                                                  *)
 (********************************************************************)

-open Stdlib
-
 (** Identifiers *)

 (** {2 Labels} *)

--- a/src/core/task.mli
+++ b/src/core/task.mli
@@ -11,7 +11,6 @@

 (** Proof Tasks, Cloning and Meta History *)

-open Stdlib
 open Ident
 open Ty
 open Term

--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)

-open Stdlib
 open Ident
 open Ty


--- a/src/core/ty.mli
+++ b/src/core/ty.mli
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)

-open Stdlib
 open Ident

 (** Types *)

--- a/src/ide/gconfig.mli
+++ b/src/ide/gconfig.mli
@@ -10,7 +10,6 @@
 (********************************************************************)

 open Why3
-open Whyconf

 type t =
    { mutable window_width : int;

--- a/src/parser/denv.mli
+++ b/src/parser/denv.mli
@@ -12,7 +12,6 @@
 open Stdlib
 open Ty
 open Term
-open Theory

 (** Destructive unification *)


--- a/src/why3doc/doc_def.mli
+++ b/src/why3doc/doc_def.mli
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)

-open Format
 open Why3
 open Ident


--- a/src/whyml/mlw_decl.mli
+++ b/src/whyml/mlw_decl.mli
@@ -10,7 +10,6 @@
 (********************************************************************)

 open Ident
-open Ty
 open Term
 open Mlw_ty
 open Mlw_ty.T

--- a/src/whyml/mlw_dty.mli
+++ b/src/whyml/mlw_dty.mli
@@ -11,13 +11,11 @@

 (* destructive types for program type inference *)

-open Ident
 open Ty
 open Term
 open Mlw_ty
 open Mlw_ty.T
 open Mlw_expr
-open Mlw_module

 type dreg
 type dity

--- a/src/whyml/mlw_expr.mli
+++ b/src/whyml/mlw_expr.mli
@@ -11,7 +11,6 @@

 open Stdlib
 open Ident
-open Ty
 open Term
 open Mlw_ty
 open Mlw_ty.T

--- a/src/whyml/mlw_ty.mli
+++ b/src/whyml/mlw_ty.mli
@@ -9,7 +9,6 @@
 (*                                                                  *)
 (********************************************************************)

-open Stdlib
 open Ident
 open Ty
 open Term

--- a/src/whyml/mlw_typing.mli
+++ b/src/whyml/mlw_typing.mli
@@ -10,9 +10,6 @@
 (********************************************************************)

 open Stdlib
-open Theory
-open Env
-open Ptree
 open Mlw_module

 type mlw_contents = modul Mstr.t