aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/tacinv.ml42
-rw-r--r--contrib/interface/xlate.ml4
-rwxr-xr-xcontrib/linear/ccidpc.ml410
-rw-r--r--parsing/g_ltac.ml44
-rw-r--r--parsing/g_ltacnew.ml44
-rw-r--r--parsing/pptactic.ml6
-rw-r--r--parsing/q_coqast.ml42
-rw-r--r--proofs/refiner.ml12
-rw-r--r--proofs/refiner.mli4
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--proofs/tactic_debug.ml8
-rw-r--r--proofs/tactic_debug.mli2
-rw-r--r--tactics/setoid_replace.ml6
-rw-r--r--tactics/tacinterp.mli2
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tauto.ml47
-rw-r--r--toplevel/cerrors.ml6
-rw-r--r--translate/pptacticnew.ml14
19 files changed, 56 insertions, 45 deletions
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index 6bc310460..3137a38ad 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -528,7 +528,7 @@ let rec iterintro i =
let hypname = (string_of_id (destVar hyp)) in
let sub =
try String.sub hypname 0 4 with _ -> "" (* different than "_eq_" *) in
- if sub="_eq_" then rewriteLR hyp else tclFAIL 0)
+ if sub="_eq_" then rewriteLR hyp else tclFAIL 0 "Cannot rewrite")
)) gl)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3941d10c6..8191a0978 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -758,7 +758,8 @@ and xlate_tactic =
(xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
CT_rec_tactic_in(tl, xlate_tactic t)
| TacAtom (_, t) -> xlate_tac t
- | TacFail n -> CT_fail (CT_int n)
+ | TacFail (n,"") -> CT_fail (CT_int n)
+ | TacFail (n,s) -> xlate_error "TODO: Fail n message"
| TacId -> CT_idtac
| TacInfo t -> CT_info(xlate_tactic t)
| TacArg a -> xlate_call_or_tacarg a
@@ -1656,6 +1657,7 @@ let xlate_vernac =
match opt_positions with
None -> CT_int_list[]
| Some l -> CT_int_list(List.map (fun x -> CT_int x) l))
+ | VernacReserve _ -> xlate_error "TODO: Default Variable Type"
| VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
| VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
| VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
diff --git a/contrib/linear/ccidpc.ml4 b/contrib/linear/ccidpc.ml4
index 09b81f349..a9b3e50ee 100755
--- a/contrib/linear/ccidpc.ml4
+++ b/contrib/linear/ccidpc.ml4
@@ -206,33 +206,33 @@ let rec alpha_term bl1 bl2 p_0 p_1 =
let forAllI id gls=if is_forall_term (pf_concl gls) then
- intro_using id gls else tclFAIL 0 gls
+ intro_using id gls else tclFAIL 0 "goal is not universally quantified" gls
let forAllE id t gls =
let rgl=pf_whd_betadeltaiota gls (pf_type_of gls (mkVar id)) in
if is_forall_term rgl then
tclTHEN (generalize [mkApp (mkVar id,[|t|])]) intro gls
- else tclFAIL 0 gls
+ else tclFAIL 0 "hypothesis is not universally quantified" gls
let existE id id2 gls =
let (_,_,t)=lookup_named id (pf_hyps gls) in
if is_exist_term t then
((tclTHEN (simplest_elim (mkVar id))
(tclTHEN (intro_using id2) (dImp None)))) gls
- else tclFAIL 0 gls
+ else tclFAIL 0 "hypothesis is not existentially quantified" gls
let negE id gls =
let (_,_,t)=lookup_named id (pf_hyps gls) in
if is_not_term t then
(simplest_elim (mkVar id)) gls
- else tclFAIL 0 gls
+ else tclFAIL 0 "hypothesis is not negated" gls
(*t exist_intro_head = put_pat mmk "ex_intro"*)
let existI t gls =
if is_exist_term (pf_concl gls) then
split (Rawterm.ImplicitBindings [t]) gls
- else tclFAIL 0 gls
+ else tclFAIL 0 "goal is not existentially quantified" gls
(*
let (wc,kONT) = Evar_refiner.startWalk gls in
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 7519df465..d05827bfe 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -189,8 +189,8 @@ GEXTEND Gram
| IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
TacSolve l
| IDENT "Idtac" -> TacId
- | IDENT "Fail" -> TacFail fail_default_value
- | IDENT "Fail"; n = natural -> TacFail n
+ | IDENT "Fail"; n = [ n = natural -> n | -> fail_default_value ];
+ s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
| st = simple_tactic -> TacAtom (loc,st)
| "("; a = tactic_expr; ")" -> a
| a = tactic_arg -> TacArg a
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index dc78f5faa..2caad4680 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -110,8 +110,8 @@ GEXTEND Gram
| IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
TacSolve l
| IDENT "idtac" -> TacId
- | IDENT "fail" -> TacFail fail_default_value
- | IDENT "fail"; n = natural -> TacFail n
+ | IDENT "fail"; n = [ n = natural -> n | -> fail_default_value ];
+ s = [ s = STRING -> s | -> ""] -> TacFail (n,s)
| st = simple_tactic -> TacAtom (loc,st)
| IDENT "eval"; rtc = red_expr; "in"; c = Constr.lconstr ->
TacArg(ConstrMayEval (ConstrEval (rtc,c)))
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index fbeb697eb..c67ce496d 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -489,7 +489,7 @@ and pr0 = function
| TacFirst tl -> str "First" ++ spc () ++ pr_tactic_seq_body tl
| TacSolve tl -> str "Solve" ++ spc () ++ pr_tactic_seq_body tl
| TacId -> str "Idtac"
- | TacFail 0 -> str "Fail"
+ | TacFail (0,"") -> str "Fail"
| TacAtom (_,t) -> pr_atom0 t
| TacArg c -> pr_tacarg c
| t -> str "(" ++ prtac t ++ str ")"
@@ -497,7 +497,9 @@ and pr0 = function
(* Semi-closed atomic tactic expressions *)
and pr1 = function
| TacAtom (_,t) -> pr_atom1 t
- | TacFail n -> str "Fail " ++ int n
+ | TacFail (0,s) -> str "Fail \"" ++ str s ++ str "\""
+ | TacFail (n,"") -> str "Fail " ++ int n
+ | TacFail (n,s) -> str "Fail " ++ int n ++ str "\"" ++ str s ++ str "\""
| t -> pr0 t
(* Orelse tactic expressions (printed as if parsed associating on the right
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 2b3967707..dd1ce4ec2 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -471,7 +471,7 @@ and mlexpr_of_tactic = function
| Tacexpr.TacProgress t ->
<:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
| Tacexpr.TacId -> <:expr< Tacexpr.TacId >>
- | Tacexpr.TacFail n -> <:expr< Tacexpr.TacFail $int:string_of_int n$ >>
+ | Tacexpr.TacFail (n,s) -> <:expr< Tacexpr.TacFail $int:string_of_int n$ $str:s$ >>
(*
| Tacexpr.TacInfo t -> TacInfo (loc,f t)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 293a2434a..61fc3f3b1 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -347,10 +347,10 @@ let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
(* A special exception for levels for the Fail tactic *)
-exception FailError of int
+exception FailError of int * string
(* The Fail tactic *)
-let tclFAIL lvl g = raise (FailError lvl)
+let tclFAIL lvl s g = raise (FailError (lvl,s))
let start_tac gls =
let (sigr,g) = unpackage gls in
@@ -508,10 +508,10 @@ let tclORELSE0 t1 t2 g =
t1 g
with
| e when catchable_exception e -> t2 g
- | FailError 0 | Stdpp.Exc_located(_, FailError 0) -> t2 g
- | FailError lvl -> raise (FailError (lvl - 1))
- | Stdpp.Exc_located (s,FailError lvl) ->
- raise (Stdpp.Exc_located (s,FailError (lvl - 1)))
+ | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> t2 g
+ | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
+ | Stdpp.Exc_located (s,FailError (lvl,s')) ->
+ raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
(* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
then applies t2 *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index c0d047edb..6ea71c4db 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -119,7 +119,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic
val tclTHENFIRSTn : tactic -> tactic array -> tactic
(* A special exception for levels for the Fail tactic *)
-exception FailError of int
+exception FailError of int * string
val tclORELSE : tactic -> tactic -> tactic
val tclREPEAT : tactic -> tactic
@@ -130,7 +130,7 @@ val tclTRY : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL : int -> tactic
+val tclFAIL : int -> string -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1c6d7a6f6..146d4bd29 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -184,7 +184,7 @@ and ('constr,'cst,'ind,'id) gen_tactic_expr =
| TacProgress of ('constr,'cst,'ind,'id) gen_tactic_expr
| TacAbstract of ('constr,'cst,'ind,'id) gen_tactic_expr * identifier option
| TacId
- | TacFail of int
+ | TacFail of int * string
| TacInfo of ('constr,'cst,'ind,'id) gen_tactic_expr
| TacLetRecIn of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast) list * ('constr,'cst,'ind,'id) gen_tactic_expr
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 592f3a2ea..9c0b77f58 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -159,10 +159,12 @@ let db_matching_failure debug =
str "Let us try the next one...")
(* Prints an evaluation failure message for a rule *)
-let db_eval_failure debug =
+let db_eval_failure debug s =
if debug = DebugOn then
- msgnl (str "This rule has failed due to \"Fail\" tactic (level 0)!" ++
- fnl() ++ str "Let us try the next one...")
+ let s = if s="" then "no message" else "message \""^s^"\"" in
+ msgnl
+ (str "This rule has failed due to \"Fail\" tactic (" ++
+ str s ++ str ", level 0)!" ++ fnl() ++ str "Let us try the next one...")
(* An exception handler *)
let explain_logic_error = ref (fun e -> mt())
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 8c5dc9d03..82f01f461 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -54,7 +54,7 @@ val db_hyp_pattern_failure :
val db_matching_failure : debug_info -> unit
(* Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> unit
+val db_eval_failure : debug_info -> string -> unit
(* An exception handler *)
val explain_logic_error: (exn -> Pp.std_ppcmds) ref
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index e397cd0cf..e44b66bd4 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -574,10 +574,10 @@ let res_tac c a hyp =
let fin = match hyp with
| None -> Auto.full_trivial
| Some h ->
- tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0))
- (tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0))
+ tclORELSE (tclTHEN (tclTRY (apply h)) (tclFAIL 0 ""))
+ (tclORELSE (tclTHEN (tclTRY (tclTHEN (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|]))) (apply h))) (tclFAIL 0 ""))
Auto.full_trivial) in
- tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0))
+ tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_refl), [|sa.set_a; sa.set_aeq; sa.set_th;c|])))) (tclFAIL 0 ""))
(tclORELSE assumption
(tclORELSE (tclTHEN (tclTRY (apply (mkApp ((Lazy.force coq_seq_sym), [|sa.set_a; sa.set_aeq; sa.set_th|])))) assumption)
fin))
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 9d63f33ef..d3c57c45b 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -23,7 +23,7 @@ open Topconstr
(* Values for interpretation *)
type value =
- | VTactic of tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
+ | VTactic of Util.loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *)
| VRTactic of (goal list sigma * validation)
| VFun of (identifier * value) list * identifier option list *raw_tactic_expr
| VVoid
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 08004e971..f6be87bcf 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -85,7 +85,7 @@ let tclLAST_HYP = tclNTH_HYP 1
let tclTRY_sign (tac : constr->tactic) sign gl =
let rec arec = function
- | [] -> tclFAIL 0
+ | [] -> tclFAIL 0 "no applicable hypothesis"
| [s] -> tac (mkVar s) (*added in order to get useful error messages *)
| (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl)
in
@@ -97,7 +97,7 @@ let tclTRY_HYPS (tac : constr->tactic) gl =
(* OR-branch *)
let tryClauses tac =
let rec firstrec = function
- | [] -> tclFAIL 0
+ | [] -> tclFAIL 0 "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 0557be882..a32eaf54f 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -44,7 +44,7 @@ val tclTRY : tactic -> tactic
val tclINFO : tactic -> tactic
val tclCOMPLETE : tactic -> tactic
val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL : int -> tactic
+val tclFAIL : int -> string -> tactic
val tclDO : int -> tactic -> tactic
val tclPROGRESS : tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 36ee7e18a..bf9059c75 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -144,7 +144,8 @@ let reduction_not_iff=interp
Progress Unfold Coq.Init.Logic.not Coq.Init.Logic.iff in H)>>
-let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff))
+let t_reduction_not_iff =
+ Tacexpr.TacArg (valueIn (VTactic (dummy_loc,reduction_not_iff)))
let intuition_gen tac =
interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
@@ -166,9 +167,9 @@ let q_elim tac=
Generalize (H x);Clear H;$tac>>
let rec lfo n gl=
- if n=0 then (tclFAIL 0 gl) else
+ if n=0 then (tclFAIL 0 "LinearIntuition failed" gl) else
let p=if n<0 then n else (n-1) in
- let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic (lfo p)))) in
+ let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic(dummy_loc,lfo p)))) in
intuition_gen lfo_rec gl
let lfo_wrap n gl=
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 45fe9995e..d0be357d5 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -84,8 +84,10 @@ let rec explain_exn_default = function
| Nametab.GlobalizationConstantError q ->
hov 0 (str "Error:" ++ spc () ++
str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
- | Refiner.FailError i ->
- hov 0 (str "Error: Tactic failed (level " ++ int i ++ str").")
+ | Refiner.FailError (i,s) ->
+ let s = if s="" then "" else " \""^s^"\"" in
+ hov 0 (str "Error: Tactic failure" ++ str s ++
+ if i=0 then mt () else str " (level " ++ int i ++ str").")
| Stdpp.Exc_located (loc,exc) ->
hov 0 ((if loc = dummy_loc then (mt ())
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index b80ae29d6..99c4bee7d 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -281,15 +281,15 @@ and pr_atom1 env = function
(* Derived basic tactics *)
| TacOldInduction h ->
- hov 1 (str "induction" ++ pr_arg pr_quantified_hypothesis h)
+ hov 1 (str "oldinduction" ++ pr_arg pr_quantified_hypothesis h)
| TacNewInduction (h,e,ids) ->
- hov 1 (str "newinduction" ++ spc () ++
+ hov 1 (str "induction" ++ spc () ++
pr_induction_arg (pr_lconstr env) h ++
pr_opt (pr_eliminator env) e ++ pr_with_names ids)
| TacOldDestruct h ->
- hov 1 (str "destruct" ++ pr_arg pr_quantified_hypothesis h)
+ hov 1 (str "olddestruct" ++ pr_arg pr_quantified_hypothesis h)
| TacNewDestruct (h,e,ids) ->
- hov 1 (str "newdestruct" ++ spc () ++
+ hov 1 (str "destruct" ++ spc () ++
pr_induction_arg (pr_lconstr env) h ++
pr_opt (pr_eliminator env) e ++ pr_with_names ids)
| TacDoubleInduction (h1,h2) ->
@@ -462,8 +462,10 @@ let rec pr_tac env inherited tac =
hov 1 (pr_tac env (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++
pr_tac env (lorelse,E) t2),
lorelse
- | TacFail 0 -> str "fail", latom
- | TacFail n -> str "fail " ++ int n, latom
+ | TacFail (0,"") -> str "fail", latom
+ | TacFail (n,s) ->
+ str "fail" ++ (if n=0 then mt () else pr_arg int n) ++
+ (if s="" then mt() else str " \"" ++ str s ++ str "\""), latom
| TacFirst tl ->
str "first" ++ spc () ++ pr_seq_body (pr_tac env) tl, llet
| TacSolve tl ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 15:22:36 +0000