diff options
| author | Pierre-Marie Pédrot | 2020-05-02 01:20:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | c459cbd09ec16dd7e6767ac4ffe55e19747f4705 (patch) | |
| tree | 0e3a21744c892db07c50fd83833baa45478cd52f /plugins | |
| parent | a704c05e4722e9fa994d98a961eee87faa28bc4c (diff) | |
Wrap a monadic combinator in a try-with block to catch exceptions.
Moving code around uncovered this bug.
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 |