From 0827cf4c6de1df1ab5cdb457c2ca8de6001427f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 29 Oct 2016 14:18:43 +0200
Subject: Fixing error localisation bug introduced in fixing #5142
 (21e1d501e17c).

(May it fell in the case mentioned in the inner comment of Exninfo.info?)
---
 pretyping/cases.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5c9ce2624c..aa24733d9f 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -64,10 +64,11 @@ let error_wrong_numarg_inductive_loc loc env c n =
 
 let list_try_compile f l =
   let rec aux errors = function
-  | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors)
+  | [] -> if errors = [] then anomaly (str "try_find_f") else iraise (List.last errors)
   | h::t ->
       try f h
       with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+	    let e = CErrors.push e in
 	    aux (e::errors) t in
   aux [] l
 
-- 
cgit v1.2.3