From 915c8f15965fe8e7ee9d02a663fd890ef80539ad Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 23 Apr 2015 14:22:42 +0200 Subject: Using tclZEROMSG instead of tclZERO in several places. --- plugins/omega/coq_omega.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/omega/coq_omega.ml') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 37428c39d..4e2696dfd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1462,7 +1462,7 @@ let coq_omega = let path = simplify_strong (new_id,new_var_num,display_var) system in if !display_action_flag then display_action display_var path; Tacticals.New.tclTHEN prelude (replay_history tactic_normalisation path) - with NO_CONTRADICTION -> Proofview.tclZERO (UserError ("" , Pp.str"Omega can't solve this system")) + with NO_CONTRADICTION -> Tacticals.New.tclZEROMSG (Pp.str"Omega can't solve this system") end end -- cgit v1.2.3