aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml4
-rw-r--r--tactics/contradiction.ml8
-rw-r--r--tactics/coretactics.ml44
-rw-r--r--tactics/eauto.ml41
-rw-r--r--tactics/eqdecide.ml8
-rw-r--r--tactics/equality.ml12
-rw-r--r--tactics/extratactics.ml43
-rw-r--r--tactics/inv.ml4
-rw-r--r--tactics/rewrite.ml8
-rw-r--r--tactics/tacenv.ml2
-rw-r--r--tactics/tacenv.mli11
-rw-r--r--tactics/tacinterp.ml41
-rw-r--r--tactics/tacticMatching.ml28
-rw-r--r--tactics/tacticals.ml22
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.ml63
-rw-r--r--tactics/tauto.ml48
17 files changed, 120 insertions, 109 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 43aa84e7a..ef6c38bf6 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -205,7 +205,7 @@ let tclLOG (dbg,depth,trace) pp tac =
with reraise ->
let reraise = Errors.push reraise in
msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
- raise reraise
+ iraise reraise
end
| Info ->
(* For "info (trivial/auto)", we store a log trace *)
@@ -217,7 +217,7 @@ let tclLOG (dbg,depth,trace) pp tac =
with reraise ->
let reraise = Errors.push reraise in
trace := (depth, None) :: !trace;
- raise reraise
+ iraise reraise
end
(** For info, from the linear trace information, we reconstitute the part
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9a241c7ef..13742f740 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -71,9 +71,9 @@ let contradiction_context =
filter_hyp (fun typ -> is_conv_leq typ t)
(fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
end)
- begin function
+ begin function (e, info) -> match e with
| Not_found -> seek_neg rest
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end)
| _ -> seek_neg rest
in
@@ -108,9 +108,9 @@ let contradiction_term (c,lbind as cl) =
else
Proofview.tclZERO Not_found
end
- begin function
+ begin function (e, info) -> match e with
| Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
end
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 4f23e3520..dfb3def56 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -205,7 +205,7 @@ let initial_atomic () =
let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
let iter (s, t) =
let body = TacAtom (dloc, t) in
- Tacenv.register_ltac false (Id.of_string s) body
+ Tacenv.register_ltac false false (Id.of_string s) body
in
let () = List.iter iter
[ "red", TacReduce(Red false,nocl);
@@ -219,7 +219,7 @@ let initial_atomic () =
"auto", TacAuto(Off,None,[],None);
]
in
- let iter (s, t) = Tacenv.register_ltac false (Id.of_string s) t in
+ let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
List.iter iter
[ "idtac",TacId [];
"fail", TacFail(ArgArg 0,[]);
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 303c73d6b..ca1cc7506 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -228,6 +228,7 @@ module SearchProblem = struct
(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
(lgls,pptac) :: aux tacl
with e when Errors.noncritical e ->
+ let e = Errors.push e in
Refiner.catch_failerror e; aux tacl
in aux l
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index a43e99a7f..df8a018bb 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -157,9 +157,9 @@ let solveEqBranch rectype =
(tclTHEN (choose_eq eqonleft) intros_reflexivity)
end
end
- begin function
+ begin function (e, info) -> match e with
| PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
(* The tactic Decide Equality *)
@@ -184,10 +184,10 @@ let decideGralEquality =
(tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
end
end
- begin function
+ 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}."))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let decideEqualityGoal = tclTHEN intros decideGralEquality
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 536112553..9740f6c1f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -223,10 +223,10 @@ let general_elim_clause with_evars frzevars cls rew elim =
tclNOTSAMEGOAL (rewrite_elim with_evars frzevars cls rew elim)
| Some _ -> rewrite_elim with_evars frzevars cls rew elim
end
- begin function
+ begin function (e, info) -> match e with
| PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
Proofview.tclZERO (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
@@ -394,7 +394,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
lft2rgt occs (c,l) ~new_goals:[]) tac
end
begin function
- | e ->
+ | (e, info) ->
let env' = push_rel_context rels env in
let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
match match_with_equality_type t' with
@@ -402,7 +402,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
let lft2rgt = adjust_rewriting_direction args lft2rgt in
leibniz_rewrite_ebindings_clause cls lft2rgt tac c
(it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl
- | None -> Proofview.tclZERO e
+ | None -> Proofview.tclZERO ~info e
(* error "The provided term does not end with an equality or a declared rewrite relation." *)
end
end
@@ -1507,7 +1507,7 @@ let cutSubstInHyp l2r eqn id =
end
let try_rewrite tac =
- Proofview.tclORELSE tac begin function
+ Proofview.tclORELSE tac begin function (e, info) -> match e with
| ConstrMatching.PatternMatchingFailure ->
tclZEROMSG (str "Not a primitive equality here.")
| e when catchable_exception e ->
@@ -1516,7 +1516,7 @@ let try_rewrite tac =
| NothingToRewrite ->
tclZEROMSG
(strbrk "Nothing to rewrite.")
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let cutSubstClause l2r eqn cls =
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 289014a58..436a66ad2 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -627,7 +627,8 @@ let hResolve id c occ t =
Pretyping.understand env sigma t_hole
with
| Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
- let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in
+ let (e, info) = Errors.push e in
+ let loc = match Loc.get_loc info with None -> Loc.ghost | Some loc -> loc in
resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
in
let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
diff --git a/tactics/inv.ml b/tactics/inv.ml
index d0de08c27..39310798d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -472,7 +472,7 @@ let raw_inversion inv_kind id status names =
end
(* Error messages of the inversion tactics *)
-let wrap_inv_error id = function
+let wrap_inv_error id = function (e, info) -> match e with
| Indrec.RecursionSchemeError
(Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) ->
Proofview.tclENV >>= fun env ->
@@ -481,7 +481,7 @@ let wrap_inv_error id = function
pr_sort k ++
strbrk " which is not allowed for inductive definition " ++
pr_inductive env (fst i) ++ str "."))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
(* The most general inversion tactic *)
let inversion inv_kind status names id =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1245e7c29..9d9847ea5 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -2011,15 +2011,15 @@ let setoid_proof ty fn fallback =
| e ->
Proofview.tclORELSE
fallback
- begin function
+ begin function (e', info) -> match e' with
| Hipattern.NoEquationFound ->
begin match e with
- | Not_found ->
+ | (Not_found, _) ->
let rel, _, _ = decompose_app_rel env sigma concl in
not_declared env ty rel
- | _ -> Proofview.tclZERO e
+ | (e, info) -> Proofview.tclZERO ~info e
end
- | e' -> Proofview.tclZERO e'
+ | e' -> Proofview.tclZERO ~info e'
end
end
end
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 390570817..2150042a5 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -121,7 +121,7 @@ let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj
subst_function = subst_md;
classify_function = classify_md}
-let register_ltac ?(for_ml=false) local id tac =
+let register_ltac for_ml local id tac =
ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
let redefine_ltac local kn tac =
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index d65177c5c..d6f2f2cdd 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -25,10 +25,13 @@ val interp_alias : alias -> glob_tactic_expr
(** {5 Coq tactic definitions} *)
-val register_ltac : ?for_ml:bool -> bool -> Id.t -> glob_tactic_expr -> unit
-(** Register a new Ltac with the given name and body. If the boolean flag is set
- to true, then this is a local definition. It also puts the Ltac name in the
- nametab, so that it can be used unqualified. *)
+val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
+(** Register a new Ltac with the given name and body.
+
+ The first boolean indicates whether this is done from ML side, rather than
+ Coq side. If the second boolean flag is set to true, then this is a local
+ definition. It also puts the Ltac name in the nametab, so that it can be
+ used unqualified. *)
val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
(** Replace a Ltac with the given name and body. If the boolean flag is set
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fc31c3a99..dd937cf6a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -128,15 +128,15 @@ end
let dloc = Loc.ghost
-let catching_error call_trace fail e =
+let catching_error call_trace fail (e, info) =
let inner_trace =
- Option.default [] (Exninfo.get e ltac_trace_info)
+ Option.default [] (Exninfo.get info ltac_trace_info)
in
- if List.is_empty call_trace && List.is_empty inner_trace then fail e
+ if List.is_empty call_trace && List.is_empty inner_trace then fail (e, info)
else begin
assert (Errors.noncritical e); (* preserved invariant *)
let new_trace = inner_trace @ call_trace in
- let located_exc = Exninfo.add e ltac_trace_info new_trace in
+ let located_exc = (e, Exninfo.add info ltac_trace_info new_trace) in
fail located_exc
end
@@ -144,12 +144,12 @@ let catch_error call_trace f x =
try f x
with e when Errors.noncritical e ->
let e = Errors.push e in
- catching_error call_trace raise e
+ catching_error call_trace iraise e
let catch_error_tac call_trace tac =
Proofview.tclORELSE
tac
- (catching_error call_trace Proofview.tclZERO)
+ (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
let curr_debug ist = match TacStore.get ist.extra f_debug with
| None -> DebugOff
@@ -747,9 +747,9 @@ let interp_may_eval f ist env sigma = function
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
- Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () ->
+ Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () ->
str"interpretation of term " ++ pr_glob_constr_env env (fst c)));
- raise reraise
+ iraise reraise
(* Interprets a constr expression possibly to first evaluate *)
let interp_constr_may_eval ist env sigma c =
@@ -761,8 +761,8 @@ let interp_constr_may_eval ist env sigma c =
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
- Proofview.NonLogical.run (debugging_exception_step ist false reraise (fun () -> str"evaluation of term"));
- raise reraise
+ Proofview.NonLogical.run (debugging_exception_step ist false (fst reraise) (fun () -> str"evaluation of term"));
+ iraise reraise
in
begin
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
@@ -1462,9 +1462,9 @@ and interp_app loc ist fv largs : typed_generic_argument Ftactic.t =
catch_error_tac trace (val_interp ist body) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
- begin fun e ->
+ begin fun (e, info) ->
Proofview.tclLIFT (debugging_exception_step ist false e (fun () -> str "evaluation")) <*>
- Proofview.tclZERO e
+ Proofview.tclZERO ~info e
end
end >>= fun v ->
(* No errors happened, we propagate the trace *)
@@ -1553,9 +1553,9 @@ and interp_match_successes lz ist tac =
let tac = Proofview.tclONCE tac in
tac >>= fun ans -> interp_match_success ist ans
else
- let break e = match e with
+ let break (e, info) = match e with
| FailError (0, _) -> None
- | FailError (n, s) -> Some (FailError (pred n, s))
+ | FailError (n, s) -> Some (FailError (pred n, s), info)
| _ -> None
in
let tac = Proofview.tclBREAK break tac >>= fun ans -> interp_match_success ist ans in
@@ -1568,10 +1568,10 @@ and interp_match ist lz constr lmr =
begin Proofview.tclORELSE
(interp_ltac_constr ist constr)
begin function
- | e ->
+ | (e, info) ->
Proofview.tclLIFT (debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression")) <*>
- Proofview.tclZERO e
+ Proofview.tclZERO ~info e
end
end >>= fun constr ->
Ftactic.enter begin fun gl ->
@@ -1715,7 +1715,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
let (>>=) = Ftactic.bind in
begin Proofview.tclORELSE
(val_interp ist e)
- begin function
+ begin function (err, info) -> match err with
| Not_found ->
Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1726,7 +1726,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
end
<*> Proofview.tclZERO Not_found
end
- | e -> Proofview.tclZERO e
+ | err -> Proofview.tclZERO ~info err
end
end >>= fun result ->
Ftactic.enter begin fun gl ->
@@ -2348,9 +2348,8 @@ let _ =
try Proof.run_tactic env tac prf
with Logic_monad.TacticFailure e as src ->
(** Catch the inner error of the monad tactic *)
- let src = Errors.push src in
- let e = Backtrace.app_backtrace ~src ~dst:e in
- raise e
+ let (_, info) = Errors.push src in
+ iraise (e, info)
in
(** Plug back the retrieved sigma *)
let sigma = Proof.in_proof prf (fun sigma -> sigma) in
diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index c662fad0b..52fa2e4a2 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -104,6 +104,8 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
let matching_error =
Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
+let imatching_error = (matching_error, Exninfo.null)
+
(** A functor is introduced to share the environment and the
evar_map. They do not change and it would be a pity to introduce
closures everywhere just for the occasional calls to
@@ -191,12 +193,12 @@ module PatternMatching (E:StaticEnvironment) = struct
m.stream eval ctx
(** Chooses in a list, in the same order as the list *)
- let rec pick (l:'a list) e : 'a m = match l with
- | [] -> { stream = fun _ _ -> Proofview.tclZERO e }
+ let rec pick (l:'a list) (e, info) : 'a m = match l with
+ | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
| x :: l ->
{ stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) }
- let pick l = pick l matching_error
+ let pick l = pick l imatching_error
(** Declares a subsitution, a context substitution and a term substitution. *)
let put subst context terms : unit m =
@@ -234,20 +236,20 @@ module PatternMatching (E:StaticEnvironment) = struct
end
| Subterm (with_app_context,id_ctxt,p) ->
- let rec map s e =
+ let rec map s (e, info) =
{ stream = fun k ctx -> match IStream.peek s with
- | IStream.Nil -> Proofview.tclZERO e
+ | IStream.Nil -> Proofview.tclZERO ~info e
| IStream.Cons ({ ConstrMatching.m_sub ; m_ctx }, s) ->
let subst = adjust m_sub in
let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
let terms = empty_term_subst in
let nctx = { subst ; context ; terms ; lhs = () } in
match merge ctx nctx with
- | None -> (map s e).stream k ctx
+ | None -> (map s (e, info)).stream k ctx
| Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
}
in
- map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) matching_error
+ map (ConstrMatching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
(** [rule_match_term term rule] matches the term [term] with the
@@ -261,8 +263,8 @@ module PatternMatching (E:StaticEnvironment) = struct
(** [match_term term rules] matches the term [term] with the set of
matching rules [rules].*)
- let rec match_term e term rules = match rules with
- | [] -> { stream = fun _ _ -> Proofview.tclZERO e }
+ let rec match_term (e, info) term rules = match rules with
+ | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
| r :: rules ->
{ stream = fun k ctx ->
let head = rule_match_term term r in
@@ -333,8 +335,8 @@ module PatternMatching (E:StaticEnvironment) = struct
(** [match_goal hyps concl rules] matches the goal [hyps|-concl]
with the set of matching rules [rules]. *)
- let rec match_goal e hyps concl rules = match rules with
- | [] -> { stream = fun _ _ -> Proofview.tclZERO e }
+ let rec match_goal (e, info) hyps concl rules = match rules with
+ | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
| r :: rules ->
{ stream = fun k ctx ->
let head = rule_match_goal hyps concl r in
@@ -354,7 +356,7 @@ let match_term env sigma term rules =
let sigma = sigma
end in
let module M = PatternMatching(E) in
- M.run (M.match_term matching_error term rules)
+ M.run (M.match_term imatching_error term rules)
(** [match_goal env sigma hyps concl rules] matches the goal
@@ -368,4 +370,4 @@ let match_goal env sigma hyps concl rules =
let sigma = sigma
end in
let module M = PatternMatching(E) in
- M.run (M.match_goal matching_error hyps concl rules)
+ M.run (M.match_goal imatching_error hyps concl rules)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 82ec15559..5c899aefc 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -300,11 +300,11 @@ module New = struct
let tclZEROMSG ?loc msg =
let err = UserError ("", msg) in
- let err = match loc with
- | None -> err
- | Some loc -> Loc.add_loc err loc
+ let info = match loc with
+ | None -> Exninfo.null
+ | Some loc -> Loc.add_loc Exninfo.null loc
in
- tclZERO err
+ tclZERO ~info err
let catch_failerror e =
try
@@ -362,14 +362,14 @@ module New = struct
t1 <*>
Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
begin tclEXTEND (Array.to_list l1) repeat (Array.to_list l2) end
- begin function
+ begin function (e, info) -> match e with
| SizeMismatch (i,_)->
let errmsg =
str"Incorrect number of goals" ++ spc() ++
str"(expected "++int i++str(String.plural i " tactic") ++ str")"
in
tclFAIL 0 errmsg
- | reraise -> tclZERO reraise
+ | reraise -> tclZERO ~info reraise
end
end
let tclTHENSFIRSTn t1 l repeat =
@@ -385,14 +385,14 @@ module New = struct
tclINDEPENDENT begin
t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *)
begin tclDISPATCH l end
- begin function
+ begin function (e, info) -> match e with
| SizeMismatch (i,_)->
let errmsg =
str"Incorrect number of goals" ++ spc() ++
str"(expected "++int i++str(String.plural i " tactic") ++ str")"
in
tclFAIL 0 errmsg
- | reraise -> tclZERO reraise
+ | reraise -> tclZERO ~info reraise
end
end
let tclTHENLIST l =
@@ -410,7 +410,7 @@ module New = struct
tclINDEPENDENT begin
Proofview.tclIFCATCH t1
(fun () -> t2)
- (fun e -> Proofview.tclORELSE t3 (fun e' -> tclZERO e))
+ (fun (e, info) -> Proofview.tclORELSE t3 (fun e' -> tclZERO ~info e))
end
let tclIFTHENSVELSE t1 a t3 =
Proofview.tclIFCATCH t1
@@ -519,9 +519,9 @@ module New = struct
let tclTIMEOUT n t =
Proofview.tclOR
(Proofview.tclTIMEOUT n t)
- begin function
+ begin function (e, info) -> match e with
| Proofview.Timeout as e -> Proofview.tclZERO (Refiner.FailError (0,lazy (Errors.print e)))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let tclTIME s t =
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index fbdc6d94e..49cae37a7 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -156,7 +156,7 @@ module New : sig
(** [catch_failerror e] fails and decreases the level if [e] is an
Ltac error with level more than 0. Otherwise succeeds. *)
- val catch_failerror : exn -> unit tactic
+ val catch_failerror : Util.iexn -> unit tactic
val tclIDTAC : unit tactic
val tclTHEN : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 40228c4df..26fd77323 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -763,11 +763,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
Proofview.tclORELSE
(Tacticals.New.tclTHEN (Proofview.V82.tactic hnf_in_concl)
(intro_then_gen name_flag move_flag false dep_flag tac))
- begin function
+ begin function (e, info) -> match e with
| RefinerError IntroNeedsProduct ->
Proofview.tclZERO
(Errors.UserError("Intro",str "No product even after head-reduction."))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
end
@@ -805,10 +805,10 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
intro_then_gen name_flag move_flag false dep_flag
(fun id -> aux (n+1) (id::ids))
end
- begin function
+ begin function (e, info) -> match e with
| RefinerError IntroNeedsProduct ->
tac ids
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
else
tac ids
@@ -1246,12 +1246,12 @@ let default_elim with_evars clear_flag (c,_ as cx) =
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd)
(general_elim with_evars clear_flag cx elim)
end)
- begin function
+ begin function (e, info) -> match e with
| IsNonrec ->
(* For records, induction principles aren't there by default
anymore. Instead, we do a case analysis instead. *)
general_case_analysis with_evars clear_flag cx
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let elim_in_context with_evars clear_flag c = function
@@ -1452,16 +1452,18 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
in
Proofview.tclORELSE
(try_apply thm_ty0 concl_nprod)
- (function PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
+ (function (e, info) -> match e with
+ | PretypeError _|RefinerError _|UserError _|Failure _ as exn0 ->
let rec try_red_apply thm_ty =
try
(* Try to head-reduce the conclusion of the theorem *)
let red_thm = try_red_product env sigma thm_ty in
Proofview.tclORELSE
(try_apply red_thm concl_nprod)
- (function PretypeError _|RefinerError _|UserError _|Failure _ ->
+ (function (e, info) -> match e with
+ | PretypeError _|RefinerError _|UserError _|Failure _ ->
try_red_apply red_thm
- | exn -> raise exn)
+ | exn -> iraise (exn, info))
with Redelimination ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
@@ -1472,22 +1474,26 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
Tacticals.New.tclTHEN
(try_main_apply b (mkVar id))
(Proofview.V82.tactic (thin [id])))
- (fun _ -> Proofview.tclZERO (Loc.add_loc exn0 loc)) c
+ (fun _ ->
+ let info = Loc.add_loc info loc in
+ Proofview.tclZERO ~info exn0) c
else
- Proofview.tclZERO (Loc.add_loc exn0 loc) in
+ let info = Loc.add_loc info loc in
+ Proofview.tclZERO ~info exn0 in
if not (Int.equal concl_nprod 0) then
try
Proofview.tclORELSE
(try_apply thm_ty 0)
- (function PretypeError _|RefinerError _|UserError _|Failure _->
+ (function (e, info) -> match e with
+ | PretypeError _|RefinerError _|UserError _|Failure _->
tac
- | exn -> raise exn)
+ | exn -> iraise (exn, info))
with UserError _ | Exit ->
tac
else
tac
in try_red_apply thm_ty0
- | exn -> raise exn)
+ | exn -> iraise (exn, info))
end
in
Tacticals.New.tclTHENLIST [
@@ -1570,7 +1576,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
with e when Errors.noncritical e ->
let e = Errors.push e in
try aux (clenv_push_prod clause)
- with NotExtensibleClause -> raise e
+ with NotExtensibleClause -> iraise e
in
aux (make_clenv_binding env sigma (d,thm) lbind)
@@ -1601,7 +1607,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let e = Errors.push e in
(descend_in_conjunctions [targetid]
(fun b id -> aux (id::idstoclear) b (mkVar id))
- (fun _ -> raise e) c)
+ (fun _ -> iraise e) c)
end
in
aux [] with_destruct d
@@ -2652,14 +2658,14 @@ let dest_intro_patterns avoid thin dest pat tac =
let safe_dest_intro_patterns avoid thin dest pat tac =
Proofview.tclORELSE
(dest_intro_patterns avoid thin dest pat tac)
- begin function
+ begin function (e, info) -> match e with
| UserError ("move_hyp",_) ->
(* May happen e.g. with "destruct x using s" with an hypothesis
which is morally an induction hypothesis to be "MoveLast" if
known as such but which is considered instead as a subterm of
a constructor to be move at the place of x. *)
dest_intro_patterns avoid thin MoveLast pat tac
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
type elim_arg_kind = RecArg | IndArg | OtherArg
@@ -4155,9 +4161,9 @@ let reflexivity_red allowred =
let reflexivity =
Proofview.tclORELSE
(reflexivity_red false)
- begin function
+ begin function (e, info) -> match e with
| NoEquationFound -> Hook.get forward_setoid_reflexivity
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let intros_reflexivity = (Tacticals.New.tclTHEN intros reflexivity)
@@ -4209,9 +4215,9 @@ let symmetry_red allowred =
let symmetry =
Proofview.tclORELSE
(symmetry_red false)
- begin function
+ begin function (e, info) -> match e with
| NoEquationFound -> Hook.get forward_setoid_symmetry
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
@@ -4232,9 +4238,9 @@ let symmetry_in id =
[ intro_replacing id;
Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
end
- begin function
+ begin function (e, info) -> match e with
| NoEquationFound -> Hook.get forward_setoid_symmetry_in id
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
end
@@ -4306,9 +4312,9 @@ let transitivity_red allowred t =
let transitivity_gen t =
Proofview.tclORELSE
(transitivity_red false t)
- begin function
+ begin function (e, info) -> match e with
| NoEquationFound -> Hook.get forward_setoid_transitivity t
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let etransitivity = transitivity_gen None
@@ -4365,9 +4371,8 @@ let abstract_subproof id gk tac =
which is an error irrelevant to the proof system (in fact it
means that [e] comes from [tac] failing to yield enough
success). Hence it reraises [e]. *)
- let src = Errors.push src in
- let e = Backtrace.app_backtrace ~src ~dst:e in
- raise e
+ let (_, info) = Errors.push src in
+ iraise (e, info)
in
let cd = Entries.DefinitionEntry const in
let decl = (cd, IsProof Lemma) in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 346f560f8..075f66751 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -314,10 +314,10 @@ let intuition_gen ist flags tac =
let tauto_intuitionistic flags =
Proofview.tclORELSE
(intuition_gen (default_ist ()) flags <:tactic<fail>>)
- begin function
+ begin function (e, info) -> match e with
| Refiner.FailError _ | UserError _ ->
Proofview.tclZERO (UserError ("tauto" , str "tauto failed."))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let coq_nnpp_path =
@@ -327,9 +327,9 @@ let coq_nnpp_path =
let tauto_classical flags nnpp =
Proofview.tclORELSE
(Tacticals.New.tclTHEN (apply nnpp) (tauto_intuitionistic flags))
- begin function
+ begin function (e, info) -> match e with
| UserError _ -> Proofview.tclZERO (UserError ("tauto" , str "Classical tauto failed."))
- | e -> Proofview.tclZERO e
+ | e -> Proofview.tclZERO ~info e
end
let tauto_gen flags =
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 19:53:49 +0000