aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/leminv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/leminv.mli')
-rw-r--r--tactics/leminv.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 16695fcd7..36aa5e67f 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -7,11 +7,8 @@
(************************************************************************)
open Loc
-open Pp
open Names
open Term
-open Glob_term
-open Proof_type
open Constrexpr
open Misctypes