From 5421b17f22b09ecca688a989a268385005dad01b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 15 Dec 2018 12:11:56 +0100
Subject: Add Map.find_opt

---
 engine/evd.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 7bc3be87a4..31c326df6a 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -601,19 +601,19 @@ let is_defined d e = EvMap.mem e d.defn_evars
 
 let is_undefined d e = EvMap.mem e d.undf_evars
 
-let existential_value d (n, args) =
-  let info = find d n in
-  match evar_body info with
-  | Evar_defined c ->
-    instantiate_evar_array info c args
-  | Evar_empty ->
-    raise NotInstantiatedEvar
+let existential_opt_value d (n, args) =
+  match EvMap.find_opt n d.defn_evars with
+  | None -> None
+  | Some info ->
+    match evar_body info with
+    | Evar_defined c -> Some (instantiate_evar_array info c args)
+    | Evar_empty -> None (* impossible but w/e *)
 
-let existential_value0 = existential_value
+let existential_value d ev = match existential_opt_value d ev with
+  | None -> raise NotInstantiatedEvar
+  | Some v -> v
 
-let existential_opt_value d ev =
-  try Some (existential_value d ev)
-  with NotInstantiatedEvar -> None
+let existential_value0 = existential_value
 
 let existential_opt_value0 = existential_opt_value
 
-- 
cgit v1.2.3