Catch more errors in Unification.abstract_list_all

This improves the error message on the example for #13171, however we
may question whether there should be an error at all.

4 files changed, 7 insertions, 7 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
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 45997e9a66..714d68165e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -54,7 +54,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
@@ -132,7 +132,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
-      constr -> constr list -> (env * type_error) option -> 'b
+      constr -> constr list -> (env * pretype_error) option -> 'b
 
 val error_wrong_abstraction_type :  env -> Evd.evar_map ->
       Name.t -> constr -> types -> types -> 'b
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 =
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a9de01bfd0..5f7eb78a40 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
     let info = Evar.Map.find ev undef in
     explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr
 
-let explain_pretype_error env sigma err =
+let rec explain_pretype_error env sigma err =
   let env = Evardefine.env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env sigma in
   match err with
@@ -893,7 +893,7 @@ let explain_pretype_error env sigma err =
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n
   | CannotFindWellTypedAbstraction (p,l,e) ->
       explain_cannot_find_well_typed_abstraction env sigma p l
-        (Option.map (fun (env',e) -> explain_type_error env' sigma e) e)
+        (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e)
   | WrongAbstractionType (n,a,t,u) ->
       explain_wrong_abstraction_type env sigma n a t u
   | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n