aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.ml')
-rw-r--r--proofs/proofview.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bcd51fe2b1..c18c48744e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -335,6 +335,7 @@ let tclEXTEND tacs1 rtac tacs2 env =
open Pretype_errors
let rec catchable_exception = function
| Loc.Exc_located(_,e) -> catchable_exception e
+ | Proof_type.LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _
| Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
| Indrec.RecursionSchemeError _