From 2845bc2712604a3fab3b3a8497bb29b38acf2777 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 20 Oct 2019 22:17:03 +0200
Subject: chore: Enclose the […get_reflexive_proof_ssr…] call in a
 try/with->assert false

as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
---
 plugins/ssr/ssrfwd.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'plugins')

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 =
-- 
cgit v1.2.3