aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/equality.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index fd1053b7db..9bd3254ec3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -27,17 +27,14 @@ open Tacmach
open Proof_type
open Logic
open Evar_refiner
-open Wcclausenv
open Pattern
open Matching
open Hipattern
open Tacexpr
open Tacticals
open Tactics
-open Tacinterp
open Tacred
open Rawterm
-open Vernacinterp
open Coqlib
open Vernacexpr
open Setoid_replace