aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretype_errors.mli
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretype_errors.mli')
-rw-r--r--pretyping/pretype_errors.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 7cef14339..c303d5d94 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -45,8 +45,8 @@ type pretype_error =
| UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option
| CannotUnify of constr * constr * unification_error option
| CannotUnifyLocal of constr * constr * constr
- | CannotUnifyBindingType of Constr.constr * Constr.constr
- | CannotGeneralize of Constr.constr
+ | CannotUnifyBindingType of constr * constr
+ | CannotGeneralize of constr
| NoOccurrenceFound of constr * Id.t option
| CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
| WrongAbstractionType of Name.t * constr * types * types