From e50a6195097c0d15c839c5403c1d02511afd54e4 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Mon, 19 Apr 2021 11:08:03 +0200
Subject: Check for existence before using `Global.lookup_constant` instead of
 catching `Not_found`

`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
---
 tactics/equality.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 633b9da053..497ce4ae1a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -379,11 +379,10 @@ let find_elim hdcncl lft2rgt dep cls ot =
             let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
             let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in
             let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
-            try
-              let _ = Global.lookup_constant c1' in c1'
-            with Not_found ->
+            if not (Environ.mem_constant c1' (Global.env ())) then
               user_err ~hdr:"Equality.find_elim"
-                (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
+                (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".");
+            c1'
           end
         | _ ->
           begin match if is_eq then eq_elimination_ref false sort else None with
-- 
cgit v1.2.3