From 0fb0666eedf4a7e7b806a0e7aff87c6d80b022a9 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 26 Jan 2024 16:54:10 +0100 Subject: [PATCH] add catches --- src/coq_elpi_vernacular.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 3e23c7711..45ac7e1c3 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -602,6 +602,9 @@ module Interp = struct end with e -> let e = Exninfo.capture e in Vernacstate.Synterp.unfreeze final_synterp_state; + (match fst e with + | CErrors.UserError _ -> () + | _ -> Feedback.msg_debug Pp.(str "elpi lets escape exception: " ++ CErrors.print (fst e))); Exninfo.iraise e) let run_in_program ?program ~syndata query = @@ -639,7 +642,9 @@ let run_tactic_common loc ?(static_check=false) program ~main ?(atts=[]) () = | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD sigma solution | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps") | API.Execute.Failure -> elpi_fails program - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> tclFAILn level msg) + | exception (Coq_elpi_utils.LtacFail (level, msg)) -> tclFAILn level msg + (*| exception (CErrors.UserError _ as e) -> Exninfo.iraise (Exninfo.capture e) *) + | exception e -> let e = Exninfo.capture e in (Feedback.msg_debug Pp.(str "elpi lets escape exception: " ++ CErrors.print (fst e)); Exninfo.iraise e)) tclIDTAC let run_tactic loc program ~atts _ist args =