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/extraction/mlutil.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/extraction/mlutil.ml')

diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index cfdaac710b..268d4bf9e9 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1525,8 +1525,7 @@ let inline_test r t =
   else
     let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in
     let has_body =
-      try constant_has_body (Global.lookup_constant c)
-      with Not_found -> false
+      Environ.mem_constant c (Global.env()) && constant_has_body (Global.lookup_constant c)
     in
     has_body &&
       (let t1 = eta_red t in
-- 
cgit v1.2.3