diff options
| author | Pierre-Marie Pédrot | 2019-08-29 14:39:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-29 14:39:59 +0200 |
| commit | 60b9352656b95b7e5c46c9f28fec3a171f3fc74a (patch) | |
| tree | fec69b141cf2e71dd9789567b001ca3df55c776b /plugins/funind/indfun.ml | |
| parent | 737955a82676cab8de7283bf23db3962dd6a3792 (diff) | |
| parent | 94c8f42eea1c36f582fe2390680de75634324c85 (diff) | |
Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exception names
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 2937ae5d14..a205c0744a 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -95,7 +95,8 @@ let functional_induction with_clean c princl pat = (* We need to refresh gl due to the updated evar_map in princ *) Proofview.Goal.enter_one (fun gl -> Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args)) - | _ -> raise (UserError(None,str "functional induction must be used with a function" )) + | _ -> + CErrors.user_err (str "functional induction must be used with a function" ) end | Some ((princ,binding)) -> Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args) |