From c459cbd09ec16dd7e6767ac4ffe55e19747f4705 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 May 2020 01:20:35 +0200
Subject: Wrap a monadic combinator in a try-with block to catch exceptions.

Moving code around uncovered this bug.
---
 plugins/ssr/ssrcommon.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 95a0790ff3..a0d90dcf0d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1321,7 +1321,8 @@ end
 
 let tacREDUCE_TO_QUANTIFIED_IND ty =
   tacSIGMA >>= fun gl ->
-  tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty)
+  try tclUNIT (Tacmach.pf_reduce_to_quantified_ind gl ty)
+  with e -> tclZERO e
 
 let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g ->
   let sigma, env = Goal.sigma g, Goal.env g in
-- 
cgit v1.2.3