aboutsummaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 207a03d80f..ccfb508964 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -134,8 +134,8 @@ let abstract_list_all env evd typ c l =
| Type_errors.TypeError (env',x) ->
(* FIXME: plug back the typing information *)
error_cannot_find_well_typed_abstraction env evd p l None
- | Pretype_errors.PretypeError (env',evd,TypingError x) ->
- error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
+ | Pretype_errors.PretypeError (env',evd,e) ->
+ error_cannot_find_well_typed_abstraction env evd p l (Some (env',e)) in
evd,(p,typp)
let set_occurrences_of_last_arg n =