diff options
| author | Emilio Jesus Gallego Arias | 2016-08-19 01:58:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-08-19 02:01:56 +0200 |
| commit | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (patch) | |
| tree | caf22d0e607ed9e0bf9ba64d76b4c2aebce63d5a /plugins/funind/invfun.ml | |
| parent | de038270f72214b169d056642eb7144a79e6f126 (diff) | |
Remove errorlabstrm in favor of user_err
As noted by @ppedrot, the first is redundant. The patch is basically a renaming.
We didn't make the component optional yet, but this could happen in a
future patch.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 26fc88a604..ee1232013b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1043,19 +1043,19 @@ let invfun qhyp f g = functional_inversion kn hid f2 f_correct g with | Failure "" -> - errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") + user_err "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () then error "Cannot use equivalence with graph for any side of the equality" - else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) | Not_found -> if do_observe () then error "No graph found for any side of equality" - else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) + else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid) end - | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ") + | _ -> user_err "" (Ppconstr.pr_id hid ++ str " must be an equality ") end) qhyp end |