Using tclZEROMSG instead of tclZERO in several places.

1 files changed, 14 insertions, 16 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 26b54a73ea..26ff7b92fc 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 [