Using tclZEROMSG instead of tclZERO in several places.

14 files changed, 46 insertions, 54 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8884aef1c..05f4c4903 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -302,9 +302,9 @@ let rec proof_tac p : unit Proofview.tactic =
   	     Tacticals.New.tclFIRST
 	       [Tacticals.New.tclTHEN (Proofview.V82.tactic (lemma2 refine)) (proof_tac p2);
 		reflexivity;
-                Proofview.tclZERO (UserError ("Congruence" ,
+                Tacticals.New.tclZEROMSG
 		    (Pp.str
-		       "I don't know how to handle dependent equality")))]]
+		       "I don't know how to handle dependent equality")]]
   | Inject (prf,cstr,nargs,argind) ->
 	 let ti=constr_of_term prf.p_lhs in
 	 let tj=constr_of_term prf.p_rhs in
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
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46274f832..7da841571 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -131,7 +131,7 @@ let conclPattern concl pat tac =
 	try
 	  Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
 	with Constr_matching.PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
+          Tacticals.New.tclZEROMSG (str "conclPattern")
   in
    Proofview.Goal.enter (fun gl ->
      let env = Proofview.Goal.env gl in
@@ -458,7 +458,7 @@ let search d n mod_delta db_list local_db =
     (* spiwack: the test of [n] to 0 must be done independently in
        each goal. Hence the [tclEXTEND] *)
     Proofview.tclEXTEND [] begin
-      if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
+      if Int.equal n 0 then Tacticals.New.tclZEROMSG (str"BOUND 2") else
         Tacticals.New.tclORELSE0 (dbg_assumption d)
 	  (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
 	     ( Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 4eb8a7925..048bd637a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -174,7 +174,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   if cl.concl_occs != AllOccurrences &&
      cl.concl_occs != NoOccurrences
   then
-    Proofview.tclZERO (UserError("" , str"The \"at\" syntax isn't available yet for the autorewrite tactic."))
+    Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
   else
     let compose_tac t1 t2 =
       match cl.onhyps with
@@ -204,7 +204,7 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
 	*)
 	gen_auto_multi_rewrite conds tac_main lbas cl
     | _ ->
-        Proofview.tclZERO (UserError ("autorewrite",strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion."))
+        Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9b69481da..c03710e91 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -55,7 +55,7 @@ let contradiction_context =
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
     let rec seek_neg l = match l with
-      | [] ->  Proofview.tclZERO (UserError ("" , Pp.str"No such contradiction"))
+      | [] ->  Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
       | (id,_,typ)::rest ->
           let typ = nf_evar sigma typ in
 	  let typ = whd_betadeltaiota env sigma typ in
@@ -107,7 +107,7 @@ let contradiction_term (c,lbind as cl) =
             Proofview.tclZERO Not_found
         end
         begin function (e, info) -> match e with
-          | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+          | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
           | e -> Proofview.tclZERO ~info e
         end
   end
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 27c3569da..d738677e5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -609,7 +609,7 @@ TACTIC EXTEND unify
     match table with
     | None ->
       let msg = str "Hint table " ++ str base ++ str " not found" in
-      Proofview.tclZERO (UserError ("", msg))
+      Tacticals.New.tclZEROMSG msg
     | Some t ->
       let state = Hint_db.transparent_state t in
       unify ~state x y
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index c2cd9e47f..2ee4bf8e1 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -158,7 +158,7 @@ let solveEqBranch rectype =
       end
     end
     begin function (e, info) -> match e with
-      | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
+      | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -186,7 +186,7 @@ let decideGralEquality =
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."))
+          Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")
       | e -> Proofview.tclZERO ~info e
     end
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7ab8d0c3b..816b54f02 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -454,7 +454,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	(* Otherwise, if we are told to rewrite in all hypothesis via the
            syntax "* |-", we fail iff all the different rewrites fail *)
 	let rec do_hyps_atleastonce = function
-	  | [] -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Nothing to rewrite."))
+	  | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.")
 	  | id :: l ->
 	    tclIFTHENTRYELSEMUST
 	     (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
@@ -874,7 +874,7 @@ let gen_absurdity id =
   then
     simplest_elim (mkVar id)
   else
-    Proofview.tclZERO (Errors.UserError ("Equality.gen_absurdity" , str "Not the negation of an equality."))
+    tclZEROMSG (str "Not the negation of an equality.")
   end
 
 (* Precondition: eq is leibniz equality
@@ -936,7 +936,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
     let concl = Proofview.Goal.concl gl in
     match find_positions env sigma t1 t2 with
     | Inr _ ->
-	Proofview.tclZERO (Errors.UserError ("discr" , str"Not a discriminable equality."))
+	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
 	let sort = pf_apply get_type_of gl concl in
 	discr_positions env sigma u eq_clause cpath dirn sort
@@ -968,7 +968,7 @@ let onNegatedEquality with_evars tac =
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
     | _ ->
-        Proofview.tclZERO (Errors.UserError ("" , str "Not a negated primitive equality."))
+        tclZEROMSG (str "Not a negated primitive equality.")
   end
 
 let discrSimpleClause with_evars = function
@@ -1303,7 +1303,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   in
   let injectors = List.map_filter filter posns in
   if List.is_empty injectors then
-    Proofview.tclZERO (Errors.UserError ("Equality.inj" , str "Failed to decompose the equality."))
+    tclZEROMSG (str "Failed to decompose the equality.")
   else
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref)
     (Proofview.tclBIND
@@ -1319,12 +1319,12 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
   | Inl _ ->
-     Proofview.tclZERO (Errors.UserError ("Inj",strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal."))
+     tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
   | Inr [] ->
      let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
-     Proofview.tclZERO (Errors.UserError ("Equality.inj",strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion)))
+     tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
   | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
-     Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
+     tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
 	(tac (clenv_value eq_clause))
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7f0a4c660..f217cda89 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -750,7 +750,7 @@ let rec find_a_destructable_match t =
 
 let destauto t =
   try find_a_destructable_match t;
-    Proofview.tclZERO (UserError ("",  str"No destructable match found"))
+    Tacticals.New.tclZEROMSG (str "No destructable match found")
   with Found tac -> tac
 
 let destauto_in id = 
@@ -966,7 +966,7 @@ let guard tst =
     Proofview.tclUNIT ()
   else
     let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in
-    Proofview.tclZERO (Errors.UserError("guard",msg))
+    Tacticals.New.tclZEROMSG msg
 
 
 TACTIC EXTEND guard
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f29680e18..0a746d283 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1492,11 +1492,11 @@ and tactic_of_value ist vle =
         extra = TacStore.set ist.extra f_trace []; } in
       let tac = name_if_glob appl (eval_tactic ist t) in
       catch_error_tac trace tac
-  | (VFun _|VRec _) -> Proofview.tclZERO (UserError ("" , str "A fully applied tactic is expected."))
+  | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
   else if has_type vle (topwit wit_tactic) then
     let tac = out_gen (topwit wit_tactic) vle in
     eval_tactic ist tac
-  else Proofview.tclZERO (UserError ("" , str"Expression does not evaluate to a tactic."))
+  else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist llc u =
@@ -1752,10 +1752,8 @@ and interp_ltac_constr ist e : constr Ftactic.t =
     Ftactic.return cresult
   with CannotCoerceTo _ ->
     let env = Proofview.Goal.env gl in
-    Proofview.tclZERO (UserError ( "",
-      errorlabstrm ""
-      (str "Must evaluate to a closed term" ++ fnl() ++
-      str "offending expression: " ++ fnl() ++ pr_inspect env e result)))
+    Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
+      str "offending expression: " ++ fnl() ++ pr_inspect env e result)
   end
 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9b16fe3f7..17ac7a4b6 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -420,7 +420,7 @@ module New = struct
 
   (* Try the first tactic that does not fail in a list of tactics *)
   let rec tclFIRST = function
-    | [] -> tclZERO (Errors.UserError ("Tacticals.New.tclFIRST",str"No applicable tactic."))
+    | [] -> tclZEROMSG (str"No applicable tactic.")
     |  t::rest -> tclORELSE0 t (tclFIRST rest)
 
   let rec tclFIRST_PROGRESS_ON tac = function
@@ -430,10 +430,7 @@ module New = struct
 
   let rec tclDO n t =
     if n < 0 then
-      tclZERO (Errors.UserError (
-        "Refiner.tclDO",
-        str"Wrong argument : Do needs a positive integer.")
-      )
+      tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
     else if n = 0 then tclUNIT ()
     else if n = 1 then t
     else tclTHEN t (tclDO (n-1) t)
@@ -456,7 +453,7 @@ module New = struct
   let tclCOMPLETE t =
     t >>= fun res ->
       (tclINDEPENDENT
-         (tclZERO (Errors.UserError ("",str"Proof is not complete.")))
+         (tclZEROMSG (str"Proof is not complete."))
       ) <*>
         tclUNIT res
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7484139c6..b40c8d0e7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -751,8 +751,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 	     (intro_then_gen name_flag move_flag false dep_flag tac))
           begin function (e, info) -> match e with
             | RefinerError IntroNeedsProduct ->
-                Proofview.tclZERO 
-		  (Errors.UserError("Intro",str "No product even after head-reduction."))
+                Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
             | e -> Proofview.tclZERO ~info e
           end
   end
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 4b03ff249..b4c7bffa9 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -316,7 +316,7 @@ let tauto_intuitionistic flags =
     (intuition_gen (default_ist ()) flags <:tactic<fail>>)
     begin function (e, info) -> match e with
       | Refiner.FailError _ | UserError _ ->
-          Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
+          Tacticals.New.tclZEROMSG (str "tauto failed.")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -328,7 +328,7 @@ let tauto_classical flags nnpp =
   Proofview.tclORELSE
     (Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
     begin function (e, info) -> match e with
-      | UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
+      | UserError _ -> Tacticals.New.tclZEROMSG (str "Classical tauto failed.")
       | e -> Proofview.tclZERO ~info e
     end
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 26b54a73e..26ff7b92f 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -369,7 +369,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
 	     Printer.pr_constr type_of_pq ++
 	     str " first.")
           in
-          Proofview.tclZERO (Errors.UserError("",err_msg))
+          Tacticals.New.tclZEROMSG err_msg
        in
        lb_type_of_p >>= fun (lb_type_of_p,eff) ->
        let lb_args = Array.append (Array.append
@@ -456,28 +456,28 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
         )
         end
     | ([],[]) -> Proofview.tclUNIT ()
-    | _ -> Proofview.tclZERO (UserError ("" , str"Both side of the equality must have the same arity."))
+    | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.")
   in
   begin try Proofview.tclUNIT (destApp lft)
-    with DestKO ->  Proofview.tclZERO (UserError ("" , str"replace failed."))
+    with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind1,ca1) ->
   begin try Proofview.tclUNIT (destApp rgt)
-    with DestKO -> Proofview.tclZERO (UserError ("" , str"replace failed."))
+    with DestKO -> Tacticals.New.tclZEROMSG (str "replace failed.")
   end >>= fun (ind2,ca2) ->
   begin try Proofview.tclUNIT (out_punivs (destInd ind1))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct ind1)))
-        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+        with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp1,i1) ->
   begin try Proofview.tclUNIT (out_punivs (destInd ind2))
     with DestKO ->
       begin try Proofview.tclUNIT (fst (fst (destConstruct ind2)))
-        with DestKO -> Proofview.tclZERO (UserError ("" , str"The expected type is an inductive one."))
+        with DestKO -> Tacticals.New.tclZEROMSG (str "The expected type is an inductive one.")
       end
   end >>= fun (sp2,i2) ->
   if not (eq_mind sp1 sp2) || not (Int.equal i1 i2)
-  then Proofview.tclZERO (UserError ("" , str"Eq should be on the same type"))
+  then Tacticals.New.tclZEROMSG (str "Eq should be on the same type")
   else aux (Array.to_list ca1) (Array.to_list ca2)
 
 (*
@@ -610,10 +610,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                                      (ca.(1)))
                                   Auto.default_auto
                               else
-                                Proofview.tclZERO (UserError ("",str"Failure while solving Boolean->Leibniz."))
-                          | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+                                Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+                          | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
                         )
-                        | _ -> Proofview.tclZERO (UserError ("", str"Failure while solving Boolean->Leibniz."))
+                        | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
                       end
 
                     ]
@@ -733,10 +733,10 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
                                 nparrec
                                 ca'.(n-2) ca'.(n-1)
                           | _ ->
-                              Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                              Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
                         )
                         | _ ->
-                            Proofview.tclZERO (UserError ("",str"Failure while solving Leibniz->Boolean."))
+                            Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
                       end
                     ]
       end
@@ -856,15 +856,13 @@ let compute_dec_tact ind lnamesparrec nparrec =
           let c, eff = find_scheme bl_scheme_kind ind in
           Proofview.tclUNIT (mkConst c,eff) with
     Not_found ->
-      Proofview.tclZERO (UserError ("",str"Error during the decidability part, boolean to leibniz"++
-        str" equality is required."))
+      Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.")
   end >>= fun (blI,eff') ->
   begin try
           let c, eff = find_scheme lb_scheme_kind ind in
           Proofview.tclUNIT (mkConst c,eff) with
     Not_found ->
-      Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++
-        str" equality is required."))
+      Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
   end >>= fun (lbI,eff'') ->
   let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in
   Tacticals.New.tclTHENLIST [