aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactic_option.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactic_option.ml')
-rw-r--r--tactics/tactic_option.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index b846c9eb7..7989b41db 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -7,7 +7,6 @@
(************************************************************************)
open Libobject
-open Proof_type
open Pp
let declare_tactic_option ?(default=Tacexpr.TacId []) name =