aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofview.ml')
-rw-r--r--proofs/proofview.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 76af0c1e0..1365fe86e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -223,7 +223,7 @@ let apply env t sp =
(*** tacticals ***)
-let rec catchable_exception = function
+let catchable_exception = function
| Proof_errors.Exception _ -> false
| e -> Errors.noncritical e