aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/class_tactics.ml4')
-rw-r--r--tactics/class_tactics.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index b42df0109..1cf41a70a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -25,7 +25,7 @@ open Tactics
open Pattern
open Clenv
open Auto
-open Rawterm
+open Glob_term
open Hiddentac
open Typeclasses
open Typeclasses_errors