diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |