diff options
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') ) |