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/indfun.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

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

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4e0e2dc501..1221ad0bda 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -80,10 +80,12 @@ let functional_induction with_clean c princl pat =
                   (elimination_sort_of_goal gl)
               in
               let princ_ref =
-                try
+                match
                   Constrintern.locate_reference
                     (Libnames.qualid_of_ident princ_name)
-                with Not_found ->
+                with
+                | Some r -> r
+                | None ->
                   user_err
                     ( str "Cannot find induction principle for "
                     ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
-- 
cgit v1.2.3