aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/contradiction.ml4
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/eqdecide.ml4
-rw-r--r--tactics/equality.ml16
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--tactics/tacinterp.ml10
-rw-r--r--tactics/tacticals.ml9
-rw-r--r--tactics/tactics.ml3
-rw-r--r--tactics/tauto.ml44
11 files changed, 29 insertions, 35 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 46274f8329..7da8415714 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 4eb8a79256..048bd637aa 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 9b69481da9..c03710e911 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 27c3569daf..d738677e50 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 c2cd9e47f1..2ee4bf8e12 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 7ab8d0c3ba..816b54f027 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 7f0a4c6609..f217cda894 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 f29680e185..0a746d283e 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 9b16fe3f7b..17ac7a4b66 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 7484139c68..b40c8d0e74 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 4b03ff249f..b4c7bffa9c 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 12:08:43 +0000