aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
-rw-r--r--pretyping/typeclasses_errors.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index fd75781ed5..21bb5f8443 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -12,8 +12,6 @@ open Names
open EConstr
open Environ
-type contexts = Parameters | Properties
-
type typeclass_error =
| NotAClass of constr
| UnboundMethod of GlobRef.t * lident (** Class name, method *)