diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-29 00:45:16 +0200 |
| commit | 4c1260299b707bd27765b0ab365092046b134a69 (patch) | |
| tree | 22331e8562bee137a5d2eea79c0d8e3d43cb94c1 /plugins/funind/invfun.ml | |
| parent | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff) | |
| parent | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff) | |
Merge PR#512: [cleanup] Unify all calls to the error function.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8eaa9b0f5..d68bdc215 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -197,7 +197,7 @@ let generate_type evd g_to_f f graph i = let find_induction_principle evd f = let f_as_constant,u = match EConstr.kind !evd f with | Const c' -> c' - | _ -> error "Must be used with a function" + | _ -> user_err Pp.(str "Must be used with a function") in let infos = find_Function_infos f_as_constant in match infos.rect_lemma with @@ -701,7 +701,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) - with Not_found -> error "No graph found" + with Not_found -> user_err Pp.(str "No graph found") in if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs @@ -1006,6 +1006,7 @@ let functional_inversion kn hid fconst f_correct : tactic = | _ -> tclFAIL 1 (mt ()) g +let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = |