aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/cc/cctac.ml4
-rw-r--r--contrib/first-order/g_ground.ml42
-rw-r--r--contrib/first-order/ground.ml2
-rw-r--r--contrib/first-order/instances.ml6
-rw-r--r--contrib/first-order/rules.ml6
-rw-r--r--contrib/funind/tacinv.ml42
-rw-r--r--contrib/recdef/recdef.ml42
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tacticals.mli5
11 files changed, 19 insertions, 18 deletions
diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index a3e1902c0..e6ce0ad66 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -287,7 +287,7 @@ let cc_tactic additionnal_terms gls=
let _ = debug Pp.msgnl (Pp.str "Computation completed.") in
let uf=forest state in
match sol with
- None -> tclFAIL 0 "congruence failed" gls
+ None -> tclFAIL 0 (str "congruence failed") gls
| Some reason ->
debug Pp.msgnl (Pp.str "Goal solved, generating proof ...");
match reason with
@@ -318,7 +318,7 @@ let cc_tactic additionnal_terms gls=
end);
Pp.msgnl
(Pp.str " replacing metavariables by arbitrary terms.");
- tclFAIL 0 "Incomplete" gls
+ tclFAIL 0 (str "Incomplete") gls
| Contradiction dis ->
let p=build_proof uf (`Prove (dis.lhs,dis.rhs)) in
let ta=term uf dis.lhs and tb=term uf dis.rhs in
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 0db32a555..e6f7b03cb 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -41,7 +41,7 @@ let _=
let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
-let fail_solver=tclFAIL 0 "GTauto failed"
+let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
type external_env=
Ids of global_reference list
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index 00a2260c6..9f9a7e68d 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -78,7 +78,7 @@ let ground_tac solver startseq gl=
| Rforall->
let backtrack1=
if !qflag then
- tclFAIL 0 "reversible in 1st order mode"
+ tclFAIL 0 (Pp.str "reversible in 1st order mode")
else
backtrack in
forall_tac backtrack continue (re_add seq1)
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 0b371966b..eac842b86 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -138,7 +138,7 @@ let left_instance_tac (inst,id) continue seq=
match inst with
Phantom dom->
if lookup (id,None) seq then
- tclFAIL 0 "already done"
+ tclFAIL 0 (Pp.str "already done")
else
tclTHENS (cut dom)
[tclTHENLIST
@@ -152,7 +152,7 @@ let left_instance_tac (inst,id) continue seq=
tclTRY assumption]
| Real((m,t) as c,_)->
if lookup (id,Some c) seq then
- tclFAIL 0 "already done"
+ tclFAIL 0 (Pp.str "already done")
else
let special_generalize=
if m>0 then
@@ -186,7 +186,7 @@ let right_instance_tac inst continue seq=
(tclTHEN (split (Rawterm.ImplicitBindings [t]))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
- tclFAIL 0 "not implemented ... yet"
+ tclFAIL 0 (Pp.str "not implemented ... yet")
let instance_tac inst=
if (snd inst)==dummy_id then
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index 727a03000..bc4699ea1 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -58,7 +58,7 @@ let clear_global=function
let axiom_tac t seq=
try exact_no_check (constr_of_global (find_left t seq))
- with Not_found->tclFAIL 0 "No axiom link"
+ with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
tclIFTHENELSE
@@ -68,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq=
[|constr_of_global (find_left a seq)|])];
clear_global id;
intro]
- with Not_found->tclFAIL 0 "No link")
+ with Not_found->tclFAIL 0 (Pp.str "No link"))
(wrap 1 false continue seq) backtrack
(* right connectives rules *)
@@ -168,7 +168,7 @@ let forall_tac backtrack continue seq=
(tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
backtrack))
(if !qflag then
- tclFAIL 0 "reversible in 1st order mode"
+ tclFAIL 0 (Pp.str "reversible in 1st order mode")
else
backtrack)
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 27c0658d2..bf918ba56 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -597,7 +597,7 @@ let rec iterintro i =
let sub =
try String.sub hypname 0 (String.length heq_prefix)
with _ -> "" (* different than [heq_prefix] *) in
- if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
+ if sub=heq_prefix then rewriteLR hyp else tclFAIL 0 (str "Cannot rewrite"))
)) gl)
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 1671c405a..2e62aa407 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -247,7 +247,7 @@ let list_rewrite (rev:bool) (eqs: constr list) =
tclREPEAT
(List.fold_right
(fun eq i -> tclORELSE (rewriteLR eq) i)
- (if rev then (List.rev eqs) else eqs) (tclFAIL 0 ""));;
+ (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
let base_leaf (func:global_reference) eqs expr =
(* let _ = msgnl (str "entering base_leaf") in *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4f8df90b5..cc6dc33e6 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -862,7 +862,7 @@ let compileAutoArg contac = function
then
tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac]
else
- tclFAIL 0 ((string_of_id id)^"is not a conjunction"))
+ tclFAIL 0 (pr_id id ++ str" is not a conjunction"))
ctx) g)
| UsingTDB ->
(tclTHEN
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fbd881789..7aae9f522 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -138,7 +138,7 @@ let add_rewrite_hint name ort t lcsr =
VERNAC COMMAND EXTEND HintRewrite
[ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
- [ add_rewrite_hint b o (Tacexpr.TacId "") l ]
+ [ add_rewrite_hint b o (Tacexpr.TacId []) l ]
| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
":" preident(b) ] ->
[ add_rewrite_hint b o t l ]
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 517d774d4..3b5349a4b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -91,7 +91,7 @@ let tclLAST_HYP = tclNTH_HYP 1
let tclTRY_sign (tac : constr->tactic) sign gl =
let rec arec = function
- | [] -> tclFAIL 0 "no applicable hypothesis"
+ | [] -> tclFAIL 0 (str "no applicable hypothesis")
| [s] -> tac (mkVar s) (*added in order to get useful error messages *)
| (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl)
in
@@ -133,7 +133,7 @@ let simple_clause_list_of cl gls =
(* OR-branch *)
let tryClauses tac cl gls =
let rec firstrec = function
- | [] -> tclFAIL 0 "no applicable hypothesis"
+ | [] -> tclFAIL 0 (str "no applicable hypothesis")
| [cls] -> tac cls (* added in order to get a useful error message *)
| cls::tl -> (tclORELSE (tac cls) (firstrec tl))
in
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 699c0d780..4b0e39e78 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,6 +9,7 @@
(*i $Id$ i*)
(*i*)
+open Pp
open Names
open Term
open Sign
@@ -24,7 +25,7 @@ open Tacexpr
(* Tacticals i.e. functions from tactics to tactics. *)
val tclIDTAC : tactic
-val tclIDTAC_MESSAGE : string -> tactic
+val tclIDTAC_MESSAGE : std_ppcmds -> tactic
val tclORELSE : tactic -> tactic -> tactic
val tclTHEN : tactic -> tactic -> tactic
val tclTHENSEQ : tactic list -> tactic
@@ -46,7 +47,7 @@ val tclTRY : tactic -> tactic
val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL : int -> string -> tactic
+val tclFAIL : int -> std_ppcmds -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 18:02:02 +0000