aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/auto.ml')
-rw-r--r--tactics/auto.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 9bb55977e..795582f27 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -30,13 +30,11 @@ open Tacticals
open Clenv
open Libnames
open Globnames
-open Nametab
open Smartlocate
open Libobject
open Printer
open Tacexpr
open Mod_subst
-open Misctypes
open Locus
open Proofview.Notations