aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r--pretyping/pretype_errors.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 1e8441dd8a..1dddc5622d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -48,7 +48,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
- | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+ | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option
| WrongAbstractionType of Name.t * constr * types * types
| AbstractionOverMeta of Name.t * Name.t
| NonLinearUnification of Name.t * constr