diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-25 14:31:15 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:42:01 +0200 |
| commit | 87910d7be9bd50de4db80f70c6e287c7c7994460 (patch) | |
| tree | ff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /plugins/funind/invfun.ml | |
| parent | 5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff) | |
Fix 4.04 warnings
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 29472cdef..6c0c28905 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1025,7 +1025,7 @@ let invfun qhyp f = | Not_found -> error "No graph found" | Option.IsNone -> error "Cannot use equivalence with graph!" - +exception NoFunction let invfun qhyp f g = match f with | Some f -> invfun qhyp f g @@ -1040,23 +1040,23 @@ let invfun qhyp f g = begin let f1,_ = decompose_app sigma args.(1) in try - if not (isConst sigma f1) then failwith ""; + if not (isConst sigma f1) then raise NoFunction; let finfos = find_Function_infos (fst (destConst sigma f1)) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f1 f_correct g - with | Failure "" | Option.IsNone | Not_found -> + with | NoFunction | Option.IsNone | Not_found -> try let f2,_ = decompose_app sigma args.(2) in - if not (isConst sigma f2) then failwith ""; + if not (isConst sigma f2) then raise NoFunction; let finfos = find_Function_infos (fst (destConst sigma f2)) in let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f2 f_correct g with - | Failure "" -> + | NoFunction -> user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () |