From 21e1d501e17c9989d9cd689988a510e1864f817a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Oct 2016 15:43:39 +0200
Subject: Attempt to improve error rendering in pattern-matching compilation
 (#5142).

When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.
---
 pretyping/cases.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0ac34b7186..5c9ce2624c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -62,13 +62,14 @@ let error_wrong_numarg_constructor_loc loc env c n =
 let error_wrong_numarg_inductive_loc loc env c n =
   raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n))
 
-let rec list_try_compile f = function
-  | [a] -> f a
-  | [] -> anomaly (str "try_find_f")
+let list_try_compile f l =
+  let rec aux errors = function
+  | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors)
   | h::t ->
       try f h
-      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
-	    list_try_compile f t
+      with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+	    aux (e::errors) t in
+  aux [] l
 
 let force_name =
   let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
-- 
cgit v1.2.3