aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/type_errors.mli')
-rw-r--r--kernel/type_errors.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 38d6d8b6e3..284f244f1e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -42,7 +42,7 @@ type type_error =
| WrongPredicateArity of constr * int * int
| NeedsInversion of constr * constr
-exception TypeError of path_kind * context * type_error
+exception TypeError of path_kind * env * type_error
val error_unbound_rel : path_kind -> env -> 'a Evd.evar_map -> int -> 'b