diff options
| -rw-r--r-- | contrib/funind/indfun.ml | 4 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 13 |
2 files changed, 12 insertions, 5 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index cfaa2d4d7..9a8d52eb7 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -266,7 +266,7 @@ let derive_inversion fix_names = ) with e -> msg_warning - (str "Cannot define correction of function and graph" ++ + (str "Cannot built inversion information" ++ if do_observe () then Cerrors.explain_exn e else mt ()) with _ -> () @@ -518,7 +518,7 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl = (None:Vernacexpr.decl_notation) | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> error - ("Cannot use mutual definition with well-founded recursion") + ("Cannot use mutual definition with well-founded recursion or measure") ) (List.combine fixpoint_exprl recdefs) in diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index a4c379bae..40c90f5a1 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -975,10 +975,17 @@ let invfun qhyp f g = functional_inversion kn hid f2 f_correct g with | Failure "" -> - errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function") + errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function") | Failure "out_some" -> - error "Cannot use equivalence with graph for any side of equality" - | Not_found -> error "No graph found for any side of equality" + 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) + | 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) end | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ") ) |