diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssr/ssrfwd.ml | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 3401a49bf3..485ec667d6 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -365,9 +365,16 @@ let intro_lock ipats = let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in let rel_args = Array.sub args lm2 2 in let sigma, refl = - (* this could raise Not_found, but this should never occur in - practice given ssrclasses.v, so we put no try/with block *) - Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel in + try + Ssrclasses.get_reflexive_proof_ssr env sigma carrier rel + (* could raise Not_found--this can't occur actually: + at that point, either [Ssrequality.ssr_is_setoid] + holds or the relation is [Coq.Init.Logic.iff], + and [Coq.ssr.ssrclasses] was necessarily required + so we know that in the environment, the relation + has an instance of [Coq.ssr.ssrclasses.Reflexive] + *) + with Not_found -> assert false in let sigma, under_rel = Ssrcommon.mkSsrConst "Under_rel" env sigma in let sigma, under_from_rel = |