aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 699b4f5ff..b150f9748 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -6,10 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Vernacexpr
open Names
-open Feedback
-open Loc
(** state-transaction-machine interface *)