aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
-rw-r--r--pretyping/typeclasses_errors.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 79f0678ff..fd709763d 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -15,7 +15,8 @@ open Environ
open Nametab
open Mod_subst
open Topconstr
-open Util
+open Errors
+open Pp
open Libnames
type contexts = Parameters | Properties