aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/obligations.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/obligations.mli')
-rw-r--r--toplevel/obligations.mli4
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 04292422c..746b4ed14 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -7,15 +7,11 @@
(************************************************************************)
open Environ
-open Tacmach
open Term
open Evd
open Names
open Pp
-open Util
-open Tacinterp
open Globnames
-open Proof_type
open Vernacexpr
open Decl_kinds
open Tacexpr