diff options
| author | Pierre-Marie Pédrot | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /plugins/funind/invfun.ml | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0178c44d09..c8b4e48337 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1000,7 +1000,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (CErrors.UserError("",str "Not a function")) + | _ -> raise (CErrors.UserError(None,str "Not a function")) in try let finfos = find_Function_infos f in @@ -1045,19 +1045,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 |