aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r--tactics/tactics.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a5f88c929..fda84e6f5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -26,7 +26,6 @@ open Pfedit
open Tacred
open Genredexpr
open Tacmach
-open Proof_type
open Logic
open Clenv
open Clenvtac
@@ -43,7 +42,6 @@ open Unification
open Locus
open Locusops
open Misctypes
-open Miscops
open Proofview.Notations
exception Bound