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/romega | |
| parent | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (diff) | |
| parent | 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb (diff) | |
Merge PR#512: [cleanup] Unify all calls to the error function.
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 2 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index c2d7d5050..6479c683b 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -28,7 +28,7 @@ let romega_tactic unsafe l = | "positive" -> eval_tactic "zify_positive" | "N" -> eval_tactic "zify_N" | "Z" -> eval_tactic "zify_op" - | s -> CErrors.error ("No ROmega knowledge base for type "^s)) + | s -> CErrors.user_err Pp.(str ("No ROmega knowledge base for type "^s))) (Util.List.sort_uniquize String.compare l) in Tacticals.New.tclTHEN diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index e56605076..fdcd62299 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -1042,5 +1042,5 @@ let total_reflexive_omega_tactic unsafe = let systems_list = destructurate_hyps full_reified_goal in if !debug then display_systems systems_list; resolution unsafe env reified_goal systems_list - with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system" + with NO_CONTRADICTION -> CErrors.user_err Pp.(str "ROmega can't solve this system") end } |