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, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2c4201f99..11bb6b436 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -24,7 +24,7 @@ open Libnames
open Evd
open Pfedit
open Tacred
-open Rawterm
+open Glob_term
open Tacmach
open Proof_type
open Logic