Merge PR #14131: Check for existence before using `Global.lookup_constant` instead of catching `Not_found`

Reviewed-by: ppedrot

1 files changed, 3 insertions, 4 deletions

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