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`.
---
 plugins/funind/gen_principle.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index cbdebb7bbc..6236a5147d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -2058,13 +2058,12 @@ let make_graph (f_ref : GlobRef.t) =
   let sigma = Evd.from_env env in
   let c, c_body =
     match f_ref with
-    | GlobRef.ConstRef c -> (
-      try (c, Global.lookup_constant c)
-      with Not_found ->
+    | GlobRef.ConstRef c ->
+      if Environ.mem_constant c (Global.env ()) then (c, Global.lookup_constant c) else
         CErrors.user_err
           Pp.(
             str "Cannot find "
-            ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c)) )
+            ++ Printer.pr_leconstr_env env sigma (EConstr.mkConst c))
     | _ -> CErrors.user_err Pp.(str "Not a function reference")
   in
   match Global.body_of_constant_body Library.indirect_accessor c_body with
-- 
cgit v1.2.3