diff options
| author | Enrico Tassi | 2021-03-19 12:27:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-04-07 19:59:46 +0200 |
| commit | b47931125432df88171c7e8a879294508a603aa9 (patch) | |
| tree | 64dca669a00da9d64f1ad687e9f18c65b69ec3c0 /plugins/funind/indfun.ml | |
| parent | 59d0462f35818c12a0727a560d7b9ecf2ceea994 (diff) | |
cleanup: less exceptions, removal of try_interp_name_alias
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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') ) |