aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/evar_tactics.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/evar_tactics.ml')
-rw-r--r--tactics/evar_tactics.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 992fdc915..f1341762a 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -7,7 +7,8 @@
(************************************************************************)
open Term
-open Util
+open Pp
+open Errors
open Evar_refiner
open Tacmach
open Tacexpr