From 34e1aeef7718dd3042ef22cd1ded9d9eb65cfd87 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Oct 2020 15:40:31 +0200
Subject: 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.
---
 vernac/himsg.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

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
-- 
cgit v1.2.3