From 9d319872a1668775ba1d72ae856f46fd7f082bb9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 28 Aug 2020 15:15:00 +0200
Subject: par: print relevant subgoal when failing

Fix (partial) #5502
---
 stm/stm.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index c94a6d3a5d..9999e66c45 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1922,7 +1922,8 @@ end = struct (* {{{ *)
                     str" solves the goal and leaves no unresolved existential variables. The following" ++
                     str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key sigma) (Evar.Set.elements evars))
        end) ()
-    with e when CErrors.noncritical e -> RespError (CErrors.print e)
+    with e when CErrors.noncritical e ->
+      RespError (CErrors.print e ++ spc() ++ str "(for subgoal "++int (fst r_ast) ++ str ")")
 
   let name_of_task { t_name } = t_name
   let name_of_request { r_name } = r_name
-- 
cgit v1.2.3