From b47931125432df88171c7e8a879294508a603aa9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 19 Mar 2021 12:27:14 +0100
Subject: cleanup: less exceptions, removal of try_interp_name_alias

---
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3234d40f73..7d19c443e9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -930,8 +930,8 @@ let do_replace (evd : Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num
           (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
           let evd', res =
             Evd.fresh_global (Global.env ()) !evd
-              (Constrintern.locate_reference
-                 (qualid_of_ident equation_lemma_id))
+              (Option.get (Constrintern.locate_reference
+                 (qualid_of_ident equation_lemma_id)))
           in
           evd := evd';
           let sigma, _ =
-- 
cgit v1.2.3