aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/rewrite.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2c6e7e736a..b67aee7f77 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -33,7 +33,6 @@ open Locus
open Locusops
open Decl_kinds
open Elimschemes
-open Goal
open Environ
open Tacinterp
open Termops