aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/exninfo.ml7
-rw-r--r--clib/exninfo.mli2
-rw-r--r--doc/changelog/12-misc/11755-exn+tclfail.rst4
-rw-r--r--engine/proofview.ml22
-rw-r--r--plugins/ltac/g_class.mlg4
-rw-r--r--plugins/ltac/rewrite.ml38
-rw-r--r--plugins/ltac/tacinterp.ml60
-rw-r--r--plugins/ltac/tactic_matching.ml10
-rw-r--r--plugins/omega/coq_omega.ml8
-rw-r--r--plugins/ssr/ssrview.ml4
-rw-r--r--proofs/clenvtac.ml4
-rw-r--r--proofs/proof.ml8
-rw-r--r--proofs/refine.ml5
-rw-r--r--tactics/auto.ml18
-rw-r--r--tactics/autorewrite.ml7
-rw-r--r--tactics/class_tactics.ml49
-rw-r--r--tactics/contradiction.ml17
-rw-r--r--tactics/eauto.ml4
-rw-r--r--tactics/elim.ml3
-rw-r--r--tactics/eqdecide.ml4
-rw-r--r--tactics/equality.ml24
-rw-r--r--tactics/hints.ml4
-rw-r--r--tactics/tacticals.ml48
-rw-r--r--tactics/tacticals.mli4
-rw-r--r--tactics/tactics.ml89
-rw-r--r--user-contrib/Ltac2/tac2match.ml10
26 files changed, 313 insertions, 144 deletions
diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index 621f7e615f..07b7f47529 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -117,3 +117,10 @@ let capture e =
e, add info backtrace_info bt
else
e, info e
+
+let reify () =
+ if !is_recording then
+ let bt = Printexc.get_callstack 50 in
+ add null backtrace_info bt
+ else
+ null
diff --git a/clib/exninfo.mli b/clib/exninfo.mli
index 55f0662431..08395f59f4 100644
--- a/clib/exninfo.mli
+++ b/clib/exninfo.mli
@@ -79,3 +79,5 @@ val capture : exn -> iexn
val iraise : iexn -> 'a
(** Raise the given enriched exception. *)
+
+val reify : unit -> info
diff --git a/doc/changelog/12-misc/11755-exn+tclfail.rst b/doc/changelog/12-misc/11755-exn+tclfail.rst
new file mode 100644
index 0000000000..800cc09e01
--- /dev/null
+++ b/doc/changelog/12-misc/11755-exn+tclfail.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ Backtrace information for tactics has been improved
+ (`#11755 <https://github.com/coq/coq/pull/11755>`_,
+ by Emilio Jesus Gallego Arias).
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2e036be9e3..de38104ecd 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -261,13 +261,9 @@ module Monad = Proof
(** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO ?info e =
+let tclZERO ?(info=Exninfo.null) e =
if not (CErrors.noncritical e) then
CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
- let info = match info with
- | None -> Exninfo.null
- | Some info -> info
- in
Proof.zero (e, info)
(** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
@@ -323,9 +319,10 @@ let tclEXACTLY_ONCE e t =
split t >>= function
| Nil (e, info) -> tclZERO ~info e
| Cons (x,k) ->
- Proof.split (k (e, Exninfo.null)) >>= function
- | Nil _ -> tclUNIT x
- | _ -> tclZERO MoreThanOneSuccess
+ let info = Exninfo.null in
+ Proof.split (k (e, Exninfo.null)) >>= function
+ | Nil _ -> tclUNIT x
+ | _ -> tclZERO ~info MoreThanOneSuccess
(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
@@ -359,7 +356,7 @@ end
is restored at the end of the tactic). If the range [i]-[j] is not
valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
let tclFOCUS ?nosuchgoal i j t =
- let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
+ let nosuchgoal ~info = Option.default (tclZERO ~info (NoSuchGoals (j+1-i))) nosuchgoal in
let open Proof in
Pv.get >>= fun initial ->
try
@@ -368,7 +365,9 @@ let tclFOCUS ?nosuchgoal i j t =
t >>= fun result ->
Pv.modify (fun next -> unfocus context next) >>
return result
- with CList.IndexOutOfRange -> nosuchgoal
+ with CList.IndexOutOfRange as exn ->
+ let _, info = Exninfo.capture exn in
+ nosuchgoal ~info
let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
@@ -907,7 +906,8 @@ let tclPROGRESS t =
if not test then
tclUNIT res
else
- tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
+ let info = Exninfo.reify () in
+ tclZERO ~info (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
let _ = CErrors.register_handler begin function
| Logic_monad.Tac_Timeout ->
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 81e745b714..35c90444b1 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -142,7 +142,9 @@ let progress_evars t =
let sigma = Tacmach.New.project gl' in
let newconcl = Proofview.Goal.concl gl' in
if eq_constr_mod_evars sigma concl newconcl
- then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
+ then
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (Pp.str"No progress made (modulo evars)")
else Proofview.tclUNIT ()
end
in t <*> check
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index d6b2a17882..4bc8d61258 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1566,7 +1566,8 @@ let assert_replacing id newt tac =
Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
let newfail n s =
- Proofview.tclZERO (Refiner.FailError (n, lazy s))
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let open Proofview.Notations in
@@ -1576,8 +1577,10 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let treat sigma res =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
- | Some None -> if progress then newfail 0 (str"Failed to progress")
- else Proofview.tclUNIT ()
+ | Some None ->
+ if progress
+ then newfail 0 (str"Failed to progress")
+ else Proofview.tclUNIT ()
| Some (Some res) ->
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
@@ -1641,7 +1644,9 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let tactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
- with e when CErrors.noncritical e -> Tacticals.New.tclFAIL 0 (str"Setoid library not loaded")
+ with e when CErrors.noncritical e ->
+ let _, info = Exninfo.capture e in
+ Tacticals.New.tclFAIL ~info 0 (str"Setoid library not loaded")
let cl_rewrite_clause_strat progress strat clause =
tactic_init_setoid () <*>
@@ -1650,10 +1655,11 @@ let cl_rewrite_clause_strat progress strat clause =
(cl_rewrite_clause_newtac ~progress strat clause)
(fun (e, info) -> match e with
| RewriteFailure e ->
- tclZEROMSG (str"setoid rewrite failed: " ++ e)
+ tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
| Refiner.FailError (n, pp) ->
- tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp)
- | e -> Proofview.tclZERO ~info e))
+ tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
+ | e ->
+ Proofview.tclZERO ~info e))
(** Setoid rewriting when called with "setoid_rewrite" *)
let cl_rewrite_clause l left2right occs clause =
@@ -2109,7 +2115,7 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals =
(cl_rewrite_clause_newtac ~progress:true ~abs:(Some abs) ~origsigma strat cl)))
(fun (e, info) -> match e with
| RewriteFailure e ->
- tclFAIL 0 (str"setoid rewrite failed: " ++ e)
+ tclFAIL ~info 0 (str"setoid rewrite failed: " ++ e)
| e -> Proofview.tclZERO ~info e)
end
@@ -2117,8 +2123,8 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite
(** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
-let not_declared env sigma ty rel =
- tclFAIL 0
+let not_declared ~info env sigma ty rel =
+ tclFAIL ~info 0
(str" The relation " ++ Printer.pr_econstr_env env sigma rel ++ str" is not a declared " ++
str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
@@ -2135,7 +2141,10 @@ let setoid_proof ty fn fallback =
let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
- with e -> Proofview.tclZERO e
+ with e ->
+ (* XXX what is the right test here as to whether e can be converted ? *)
+ let e, info = Exninfo.capture e in
+ Proofview.tclZERO ~info e
end
begin function
| e ->
@@ -2145,9 +2154,10 @@ let setoid_proof ty fn fallback =
| Hipattern.NoEquationFound ->
begin match e with
| (Not_found, _) ->
- let rel, _, _ = decompose_app_rel env sigma concl in
- not_declared env sigma ty rel
- | (e, info) -> Proofview.tclZERO ~info e
+ let rel, _, _ = decompose_app_rel env sigma concl in
+ not_declared ~info env sigma ty rel
+ | (e, info) ->
+ Proofview.tclZERO ~info e
end
| e' -> Proofview.tclZERO ~info e'
end
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6d350ade8d..5abe18e00c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -774,7 +774,9 @@ let interp_message_token ist = function
| MsgIdent {loc;v=id} ->
let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
match v with
- | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
+ | None -> Ftactic.lift (
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (Id.print id ++ str" not found."))
| Some v -> message_of_value v
let interp_message ist l =
@@ -1087,11 +1089,15 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
end
| TacFail (g,n,s) ->
let msg = interp_message ist s in
- let tac l = Tacticals.New.tclFAIL (interp_int_or_var ist n) l in
+ let tac ~info l = Tacticals.New.tclFAIL ~info (interp_int_or_var ist n) l in
let tac =
match g with
- | TacLocal -> fun l -> Proofview.tclINDEPENDENT (tac l)
- | TacGlobal -> tac
+ | TacLocal ->
+ let info = Exninfo.reify () in
+ fun l -> Proofview.tclINDEPENDENT (tac ~info l)
+ | TacGlobal ->
+ let info = Exninfo.reify () in
+ tac ~info
in
Ftactic.run msg tac
| TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac)
@@ -1174,8 +1180,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let len1 = List.length alias.Tacenv.alias_args in
let len2 = List.length l in
if len1 = len2 then tac
- else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
- expected " ++ int len1 ++ str ", found " ++ int len2)
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
+ (str "Arguments length mismatch: \
+ expected " ++ int len1 ++ str ", found " ++ int len2)
in
Ftactic.run tac (fun () -> Proofview.tclUNIT ())
@@ -1267,7 +1276,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
and interp_app loc ist fv largs : Val.t Ftactic.t =
Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let (>>=) = Ftactic.bind in
- let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
+ let fail ~info = Tacticals.New.tclZEROMSG ~info (str "Illegal tactic application.") in
if has_type fv (topwit wit_tacvalue) then
match to_tacvalue fv with
(* if var=[] and body has been delayed by val_interp, then body
@@ -1313,12 +1322,18 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
| (VFun(appl,trace,olfun,[],body)) ->
let extra_args = List.length largs in
- Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
- str (string_of_int extra_args) ++
- str " extra " ++ str (String.plural extra_args "argument") ++
- str ".")
- | VRec(_,_) -> fail
- else fail
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
+ (str "Illegal tactic application: got " ++
+ str (string_of_int extra_args) ++
+ str " extra " ++ str (String.plural extra_args "argument") ++
+ str ".")
+ | VRec(_,_) ->
+ let info = Exninfo.reify () in
+ fail ~info
+ else
+ let info = Exninfo.reify () in
+ fail ~info
(* Gives the tactic corresponding to the tactic value *)
and tactic_of_value ist vle =
@@ -1346,7 +1361,8 @@ and tactic_of_value ist vle =
let givenargs =
List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in
let numgiven = List.length givenargs in
- Tacticals.New.tclZEROMSG
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
(Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++
(match numargs with
0 -> assert false
@@ -1364,11 +1380,15 @@ and tactic_of_value ist vle =
| _ ->
Pp.str "arguments were provided for variables " ++
pr_enum Pp.str givenargs ++ Pp.str ".")
- | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+ | VRec _ ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (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
tactic_of_value ist tac
- else Tacticals.New.tclZEROMSG (str "Expression does not evaluate to a tactic.")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "Expression does not evaluate to a tactic.")
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist llc u =
@@ -1562,10 +1582,12 @@ and interp_ltac_constr ist e : EConstr.t Ftactic.t =
pr_econstr_env env sigma cresult)
end <*>
Ftactic.return cresult
- with CannotCoerceTo _ ->
+ with CannotCoerceTo _ as exn ->
+ let _, info = Exninfo.capture exn in
let env = Proofview.Goal.env gl in
- Tacticals.New.tclZEROMSG (str "Must evaluate to a closed term" ++ fnl() ++
- str "offending expression: " ++ fnl() ++ pr_inspect env e result)
+ Tacticals.New.tclZEROMSG ~info
+ (str "Must evaluate to a closed term" ++ fnl() ++
+ str "offending expression: " ++ fnl() ++ pr_inspect env e result)
end
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 525199735d..2b43b11fe1 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -186,7 +186,9 @@ module PatternMatching (E:StaticEnvironment) = struct
{ stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
(** Failure of the pattern-matching monad: no success. *)
- let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+ let fail (type a) : a m = { stream = fun _ _ ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info matching_error }
let run (m : 'a m) =
let ctx = {
@@ -209,7 +211,11 @@ module PatternMatching (E:StaticEnvironment) = struct
(** Declares a substitution, a context substitution and a term substitution. *)
let put subst context terms : unit m =
let s = { subst ; context ; terms ; lhs = () } in
- { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+ { stream = fun k ctx -> match merge s ctx with
+ | None ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info matching_error
+ | Some s -> k () s }
(** Declares a substitution. *)
let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 79d6c05e1d..3ba6365783 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1475,7 +1475,9 @@ let coq_omega =
let path = simplify_strong (new_id,new_var_num,display_var) system in
if !display_action_flag then display_action display_var path;
tclTHEN prelude (replay_history tactic_normalisation path)
- with NO_CONTRADICTION -> tclZEROMSG (Pp.str"Omega can't solve this system")
+ with NO_CONTRADICTION as e ->
+ let _, info = Exninfo.capture e in
+ tclZEROMSG ~info (Pp.str"Omega can't solve this system")
end
end
@@ -1890,7 +1892,9 @@ let destructure_goal =
end)
intro
with Undecidable -> Tactics.elim_type (Lazy.force coq_False)
- | e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ | e when Proofview.V82.catchable_exception e ->
+ let e, info = Exninfo.capture e in
+ Proofview.tclZERO ~info e
in
tclTHEN goal_tac destructure_hyps
in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 88a3e85211..ad0a31622c 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -194,9 +194,11 @@ let interp_glob ist glob = Goal.enter_one ~__LOC__ begin fun goal ->
Pp.(str"interp-out: " ++ Printer.pr_econstr_env env sigma term));
tclUNIT (env,sigma,term)
with e ->
+ (* XXX this is another catch all! *)
+ let e, info = Exninfo.capture e in
Ssrprinters.ppdebug (lazy
Pp.(str"interp-err: " ++ Printer.pr_glob_constr_env env glob));
- tclZERO e
+ tclZERO ~info e
end
(* Commits the term to the monad *)
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 0257a6f204..007d53f911 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -129,5 +129,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
try
let evd' = w_unify env evd CONV ~flags m n in
Proofview.Unsafe.tclEVARSADVANCE evd'
- with e when CErrors.noncritical e -> Proofview.tclZERO e
+ with e when CErrors.noncritical e ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info e
end
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 75aca7e7ff..175c487958 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -525,7 +525,10 @@ let solve ?with_end_tac gi info_lvl tac pr =
| None -> tac
| Some _ -> Proofview.Trace.record_info_trace tac
in
- let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+ let nosuchgoal =
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr))
+ in
let tac = let open Goal_select in match gi with
| SelectAlreadyFocused ->
let open Proofview.Notations in
@@ -537,7 +540,8 @@ let solve ?with_end_tac gi info_lvl tac pr =
Pp.(str "Expected a single focused goal but " ++
int n ++ str " goals are focused."))
in
- Proofview.tclZERO e
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info e
| SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
| SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 0bf0cd7b63..a10bbcbdd4 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -132,4 +132,7 @@ let solve_constraints =
tclENV >>= fun env -> tclEVARMAP >>= fun sigma ->
try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
Unsafe.tclEVARSADVANCE sigma
- with e -> tclZERO e
+ with e ->
+ (* XXX this is absorbing anomalies? *)
+ let info = Exninfo.reify () in
+ tclZERO ~info e
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5b06088518..681c4e910f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -137,8 +137,9 @@ let conclPattern concl pat tac =
| Some pat ->
try
Proofview.tclUNIT (Constr_matching.matches env sigma pat concl)
- with Constr_matching.PatternMatchingFailure ->
- Tacticals.New.tclZEROMSG (str "pattern-matching failed")
+ with Constr_matching.PatternMatchingFailure as exn ->
+ let _, info = Exninfo.capture exn in
+ Tacticals.New.tclZEROMSG ~info (str "pattern-matching failed")
in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -383,7 +384,9 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
let tactic = function
| Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
- | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
+ | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
| Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
@@ -395,7 +398,9 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
Proofview.Goal.enter begin fun gl ->
if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
- else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
end
| Extern tacast ->
conclPattern concl p tacast
@@ -492,7 +497,10 @@ 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 Tacticals.New.tclZEROMSG (str"BOUND 2") else
+ if Int.equal n 0 then
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (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 ac83acd726..eaefa2947a 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -154,7 +154,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
if not (Locusops.is_all_occurrences cl.concl_occs) &&
cl.concl_occs != NoOccurrences
then
- Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"The \"at\" syntax isn't available yet for the autorewrite tactic.")
else
let compose_tac t1 t2 =
match cl.onhyps with
@@ -185,7 +186,9 @@ let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl =
*)
Proofview.V82.wrap_exceptions (fun () -> gen_auto_multi_rewrite conds tac_main lbas cl)
| _ ->
- Tacticals.New.tclZEROMSG (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.")
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info
+ (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/class_tactics.ml b/tactics/class_tactics.ml
index a51fc8b347..80c76bee60 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -166,7 +166,9 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
Proofview.Goal.enter begin fun gls ->
let resolve =
try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
- with e when noncritical e -> Proofview.tclZERO e
+ with e when noncritical e ->
+ let _, info = Exninfo.capture e in
+ Proofview.tclZERO ~info e
in resolve >>= fun clenv' ->
Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
end
@@ -207,12 +209,14 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
let unify_resolve_refine poly flags gl clenv =
Proofview.tclORELSE
(unify_resolve_refine poly flags gl clenv)
- (fun ie ->
- match fst ie with
+ (fun (exn,info) ->
+ match exn with
| Evarconv.UnableToUnify _ ->
- Tacticals.New.tclZEROMSG (str "Unable to unify")
- | e ->
- Tacticals.New.tclZEROMSG (str "Unexpected error"))
+ Tacticals.New.tclZEROMSG ~info (str "Unable to unify")
+ | e when CErrors.noncritical e ->
+ Tacticals.New.tclZEROMSG ~info (str "Unexpected error")
+ | _ ->
+ Exninfo.iraise (exn,info))
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
@@ -234,10 +238,13 @@ let with_prods nprods poly (c, clenv) f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
try match clenv_of_prods poly nprods (c, clenv) gl with
- | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
| Some (diff, clenv') -> f gl (c, diff, clenv')
with e when CErrors.noncritical e ->
- Tacticals.New.tclZEROMSG (CErrors.print e) end
+ let e, info = Exninfo.capture e in
+ Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
else Proofview.Goal.enter
begin fun gl ->
if Int.equal nprods 0 then f gl (c, None, clenv)
@@ -811,7 +818,9 @@ module Search = struct
search_tac hints limit (succ depth) info
in
fun info ->
- if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx
+ if Int.equal depth (succ limit) then
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info ReachedLimitEx
else
Proofview.tclOR (hints_tac hints info kont)
(fun e -> Proofview.tclOR (intro info kont)
@@ -860,9 +869,13 @@ module Search = struct
let fix_iterative_limit limit t =
let open Proofview in
let rec aux depth =
- if Int.equal depth (succ limit) then tclZERO ReachedLimitEx
- else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth)
- | (e,ie) -> Proofview.tclZERO ~info:ie e)
+ if Int.equal depth (succ limit)
+ then
+ let info = Exninfo.reify () in
+ tclZERO ~info ReachedLimitEx
+ else tclOR (t depth) (function
+ | (ReachedLimitEx, _) -> aux (succ depth)
+ | (e,ie) -> Proofview.tclZERO ~info:ie e)
in aux 1
let eauto_tac_stuck mst ?(unique=false)
@@ -884,18 +897,18 @@ module Search = struct
| None -> fix_iterative search
| Some l -> fix_iterative_limit l search
in
- let error (e, ie) =
+ let error (e, info) =
match e with
| ReachedLimitEx ->
- Tacticals.New.tclFAIL 0 (str"Proof search reached its limit")
+ Tacticals.New.tclFAIL ~info 0 (str"Proof search reached its limit")
| NoApplicableEx ->
- Tacticals.New.tclFAIL 0 (str"Proof search failed" ++
+ Tacticals.New.tclFAIL ~info 0 (str"Proof search failed" ++
(if Option.is_empty depth then mt()
else str" without reaching its limit"))
| Proofview.MoreThanOneSuccess ->
- Tacticals.New.tclFAIL 0 (str"Proof search failed: " ++
- str"more than one success found")
- | e -> Proofview.tclZERO ~info:ie e
+ Tacticals.New.tclFAIL ~info 0 (str"Proof search failed: " ++
+ str"more than one success found")
+ | e -> Proofview.tclZERO ~info e
in
let tac = Proofview.tclOR tac error in
let tac =
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index d6be714dd9..8ad3d072ec 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -49,7 +49,9 @@ let absurd c = absurd c
(** [f] does not assume its argument to be [nf_evar]-ed. *)
let filter_hyp f tac =
let rec seek = function
- | [] -> Proofview.tclZERO Not_found
+ | [] ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info Not_found
| d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
| _::rest -> seek rest in
Proofview.Goal.enter begin fun gl ->
@@ -62,7 +64,9 @@ let contradiction_context =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let rec seek_neg l = match l with
- | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
+ | [] ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (Pp.str"No such contradiction")
| d :: rest ->
let id = NamedDecl.get_id d in
let typ = nf_evar sigma (NamedDecl.get_type d) in
@@ -83,7 +87,8 @@ let contradiction_context =
(* Checking on the fly that it type-checks *)
simplest_elim (mkApp (mkVar id,[|p|]))
| None ->
- Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type."))
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (Pp.str"Not a negated unit type."))
(Proofview.tclORELSE
(Proofview.Goal.enter begin fun gl ->
let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
@@ -123,10 +128,12 @@ let contradiction_term (c,lbind as cl) =
filter_hyp (fun c -> is_negation_of env sigma typ c)
(fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
else
- Proofview.tclZERO Not_found
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info Not_found
end
begin function (e, info) -> match e with
- | Not_found -> Tacticals.New.tclZEROMSG (Pp.str"Not a contradiction.")
+ | Not_found ->
+ Tacticals.New.tclZEROMSG ~info (Pp.str"Not a contradiction.")
| e -> Proofview.tclZERO ~info e
end
end
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7b323ee0ed..710e0a6808 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -526,5 +526,7 @@ let autounfold_one db cl =
match cl with
| Some hyp -> change_in_hyp ~check:true None (make_change_arg c') hyp
| None -> convert_concl ~check:false c' DEFAULTcast
- else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str "Nothing to unfold")
end
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 5d8698916f..415c980c2a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -160,7 +160,8 @@ let double_ind h1 h2 =
let abs =
if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else
if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else
- tclZEROMSG (Pp.str "Both hypotheses are the same.") in
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (Pp.str "Both hypotheses are the same.") in
abs >>= fun (abs_i,abs_j) ->
(tclTHEN (tclDO abs_i intro)
(onLastHypId
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 6fbd29def9..57d793b2a5 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -182,7 +182,9 @@ let match_eqdec env sigma c =
let neq = mkApp (noteq,[|mkApp (eq2,[|t;x;y|])|]) in
if eqonleft then mkApp (op,[|eq;neq|]) else mkApp (op,[|neq;eq|]) in
Proofview.tclUNIT (eqonleft,mk,c1,c2,ty)
- with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure
+ with PatternMatchingFailure as exn ->
+ let _, info = Exninfo.capture exn in
+ Proofview.tclZERO ~info PatternMatchingFailure
(* /spiwack *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 58345ac253..79b6dfe920 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -280,8 +280,9 @@ let general_elim_clause with_evars frzevars cls rew elim =
end
begin function (e, info) -> match e with
| PretypeError (env, evd, NoOccurrenceFound (c', _)) ->
- Proofview.tclZERO (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
- | e -> Proofview.tclZERO ~info e
+ Proofview.tclZERO ~info (PretypeError (env, evd, NoOccurrenceFound (c', cls)))
+ | e ->
+ Proofview.tclZERO ~info e
end
let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
@@ -1036,7 +1037,9 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
Proofview.tclUNIT
(build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath)
with
- UserError _ as ex -> Proofview.tclZERO ex
+ UserError _ as ex ->
+ let _, info = Exninfo.capture ex in
+ Proofview.tclZERO ~info ex
in
discriminator >>= fun discriminator ->
discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf ->
@@ -1052,9 +1055,10 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let env = Proofview.Goal.env gl in
match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
| Inr _ ->
- tclZEROMSG (str"Not a discriminable equality.")
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"Not a discriminable equality.")
| Inl (cpath, (_,dirn), _) ->
- discr_positions env sigma u eq_clause cpath dirn
+ discr_positions env sigma u eq_clause cpath dirn
end
let onEquality with_evars tac (c,lbindc) =
@@ -1083,7 +1087,8 @@ let onNegatedEquality with_evars tac =
(onLastHypId (fun id ->
onEquality with_evars tac (mkVar id,NoBindings)))
| _ ->
- tclZEROMSG (str "Not a negated primitive equality.")
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str "Not a negated primitive equality.")
end
let discrSimpleClause with_evars = function
@@ -1625,10 +1630,11 @@ let cutSubstInHyp l2r eqn id =
let try_rewrite tac =
Proofview.tclORELSE tac begin function (e, info) -> match e with
| Constr_matching.PatternMatchingFailure ->
- tclZEROMSG (str "Not a primitive equality here.")
+ tclZEROMSG ~info (str "Not a primitive equality here.")
| e ->
- tclZEROMSG
- (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
+ (* XXX: absorbing anomalies?? *)
+ tclZEROMSG ~info
+ (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
end
let cutSubstClause l2r eqn cls =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5fb519cc4f..a0670ef70d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1570,6 +1570,8 @@ let run_hint tac k = match warn_hint () with
else Proofview.tclTHEN (log_hint tac) (k tac.obj)
| HintStrict ->
if is_imported tac then k tac.obj
- else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
+ else
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (UserError (None, (str "Tactic failure.")))
let repr_hint h = h.obj
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 374706c8f9..a4d306c497 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -266,22 +266,36 @@ module New = struct
let tclTHEN t1 t2 =
t1 <*> t2
- let tclFAIL lvl msg =
- tclZERO (Refiner.FailError (lvl,lazy msg))
-
- let tclZEROMSG ?loc msg =
- let err = UserError (None, msg) in
+ let tclFAIL ?info lvl msg =
+ let info = match info with
+ (* If the backtrace points here it means the caller didn't save
+ the backtrace correctly *)
+ | None -> Exninfo.reify ()
+ | Some info -> info
+ in
+ tclZERO ~info (Refiner.FailError (lvl,lazy msg))
+
+ let tclZEROMSG ?info ?loc msg =
+ let info = match info with
+ (* If the backtrace points here it means the caller didn't save
+ the backtrace correctly *)
+ | None -> Exninfo.reify ()
+ | Some info -> info
+ in
let info = match loc with
- | None -> Exninfo.null
- | Some loc -> Loc.add_loc Exninfo.null loc
+ | None -> info
+ | Some loc -> Loc.add_loc info loc
in
+ let err = UserError (None, msg) in
tclZERO ~info err
let catch_failerror e =
try
Refiner.catch_failerror e;
tclUNIT ()
- with e when CErrors.noncritical e -> tclZERO e
+ with e when CErrors.noncritical e ->
+ let _, info = Exninfo.capture e in
+ tclZERO ~info e
(* spiwack: I chose to give the Ltac + the same semantics as
[Proofview.tclOR], however, for consistency with the or-else
@@ -441,8 +455,10 @@ module New = struct
(* Try the first tactic that does not fail in a list of tactics *)
let rec tclFIRST = function
- | [] -> tclZEROMSG (str"No applicable tactic.")
- | t::rest -> tclORELSE0 t (tclFIRST rest)
+ | [] ->
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"No applicable tactic.")
+ | t::rest -> tclORELSE0 t (tclFIRST rest)
let rec tclFIRST_PROGRESS_ON tac = function
| [] -> tclFAIL 0 (str "No applicable tactic")
@@ -451,7 +467,8 @@ module New = struct
let rec tclDO n t =
if n < 0 then
- tclZEROMSG (str"Wrong argument : Do needs a positive integer.")
+ let info = Exninfo.reify () in
+ tclZEROMSG ~info (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)
@@ -474,7 +491,8 @@ module New = struct
let tclCOMPLETE t =
t >>= fun res ->
(tclINDEPENDENT
- (tclZEROMSG (str"Proof is not complete."))
+ (let info = Exninfo.reify () in
+ tclZEROMSG ~info (str"Proof is not complete."))
) <*>
tclUNIT res
@@ -533,7 +551,8 @@ module New = struct
let () = check_evars env sigma_final sigma sigma_initial in
tclUNIT x
with e when CErrors.noncritical e ->
- tclZERO e
+ let e, info = Exninfo.capture e in
+ tclZERO ~info e
else
tclUNIT x
in
@@ -552,7 +571,8 @@ module New = struct
(Proofview.tclTIMEOUT n t)
begin function (e, info) -> match e with
| Logic_monad.Tac_Timeout as e ->
- Proofview.tclZERO (Refiner.FailError (0,lazy (CErrors.print e)))
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (Refiner.FailError (0,lazy (CErrors.print e)))
| e -> Proofview.tclZERO ~info e
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 01565169ca..eebe702259 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -151,9 +151,9 @@ module New : sig
(* [tclFAIL n msg] fails with [msg] as an error message at level [n]
(meaning that it will jump over [n] error catching tacticals FROM
THIS MODULE. *)
- val tclFAIL : int -> Pp.t -> 'a tactic
+ val tclFAIL : ?info:Exninfo.info -> int -> Pp.t -> 'a tactic
- val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic
+ val tclZEROMSG : ?info:Exninfo.info -> ?loc:Loc.t -> Pp.t -> 'a tactic
(** Fail with a [User_Error] containing the given message. *)
val tclOR : unit tactic -> unit tactic -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 378b6c7418..5fe87a94c5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -182,10 +182,13 @@ let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
| Some sigma -> Proofview.Unsafe.tclEVARS sigma
- | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
- | exception _ ->
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str "Not convertible")
+ | exception e ->
+ let _, info = Exninfo.capture e in
(* FIXME: Sometimes an anomaly is raised from conversion *)
- Tacticals.New.tclFAIL 0 (str "Not convertible")
+ Tacticals.New.tclFAIL ~info 0 (str "Not convertible")
end
let convert x y = convert_gen Reduction.CONV x y
@@ -301,7 +304,9 @@ let rename_hyp repl =
let init = Some (Id.Set.empty, Id.Set.empty) in
let dom = List.fold_left fold init repl in
match dom with
- | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "Not a one-to-one name mapping")
| Some (src, dst) ->
Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
@@ -1023,7 +1028,10 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
(Proofview.Unsafe.tclEVARS sigma)
(intro_then_gen name_flag move_flag force_flag dep_flag tac)
| _ ->
- begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct))
+ begin if not force_flag
+ then
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (RefinerError (env, sigma, IntroNeedsProduct))
(* Note: red_in_concl includes betaiotazeta and this was like *)
(* this since at least V6.3 (a pity *)
(* that intro do betaiotazeta only when reduction is needed; and *)
@@ -1035,7 +1043,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 (env, sigma, IntroNeedsProduct) ->
- Tacticals.New.tclZEROMSG (str "No product even after head-reduction.")
+ Tacticals.New.tclZEROMSG ~info (str "No product even after head-reduction.")
| e -> Proofview.tclZERO ~info e
end
end
@@ -1314,7 +1322,8 @@ let cut c =
know the relevance *)
match Typing.sort_of env sigma c with
| exception e when noncritical e ->
- Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
+ let _, info = Exninfo.capture e in
+ Tacticals.New.tclZEROMSG ~info (str "Not a proposition or a type.")
| sigma, s ->
let r = Sorts.relevance_of_sort s in
let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
@@ -1666,7 +1675,9 @@ let descend_in_conjunctions avoid tac (err, info) c =
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
match make_projection env sigma params cstr sign elim i n c u with
- | None -> Tacticals.New.tclFAIL 0 (mt())
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (mt())
| Some (p,pt) ->
Tacticals.New.tclTHENS
(assert_before_gen false (NamingAvoid avoid) pt)
@@ -1718,7 +1729,8 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in
Clenvtac.res_pf clause ~with_evars ~flags
with exn when noncritical exn ->
- Proofview.tclZERO exn
+ let exn, info = Exninfo.capture exn in
+ Proofview.tclZERO ~info exn
in
let rec try_red_apply thm_ty (exn0, info) =
try
@@ -1730,9 +1742,10 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
| PretypeError _|RefinerError _|UserError _|Failure _ ->
Some (try_red_apply red_thm (exn0, info))
| _ -> None)
- with Redelimination ->
+ with Redelimination as exn ->
(* Last chance: if the head is a variable, apply may try
second order unification *)
+ let exn, info = Exninfo.capture exn in
let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
let tac =
if with_destruct then
@@ -1991,7 +2004,9 @@ let assumption =
if only_eq then
let hyps = Proofview.Goal.hyps gl in
arec gl false hyps
- else Tacticals.New.tclZEROMSG (str "No such assumption.")
+ else
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "No such assumption.")
| decl::rest ->
let t = NamedDecl.get_type decl in
let concl = Proofview.Goal.concl gl in
@@ -2087,12 +2102,13 @@ let clear_body ids =
else sigma
in
Proofview.Unsafe.tclEVARS sigma
- with DependsOnBody where ->
+ with DependsOnBody where as exn ->
+ let _, info = Exninfo.capture exn in
let msg = match where with
| None -> str "Conclusion" ++ on_the_bodies ids
| Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies ids
in
- Tacticals.New.tclZEROMSG msg
+ Tacticals.New.tclZEROMSG ~info msg
in
check <*>
Refine.refine ~typecheck:false begin fun sigma ->
@@ -2306,7 +2322,8 @@ let intro_decomp_eq ?loc l thin tac id =
(fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l)
(eq,t,eq_args) (c, t)
| None ->
- Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str "Not a primitive equality here.")
end
let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
@@ -3992,13 +4009,14 @@ let specialize_eqs id =
(internal_cut true id ty')
(exact_no_check ((* refresh_universes_strict *) acc'))
else
- Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id)
+ let info = Exninfo.reify () in
+ Tacticals.New.tclFAIL ~info 0 (str "Nothing to do in hypothesis " ++ Id.print id)
end
let specialize_eqs id = Proofview.Goal.enter begin fun gl ->
let msg = str "Specialization not allowed on dependent hypotheses" in
Proofview.tclOR (clear [id])
- (fun _ -> Tacticals.New.tclZEROMSG msg) >>= fun () ->
+ (fun (_,info) -> Tacticals.New.tclZEROMSG ~info msg) >>= fun () ->
specialize_eqs id
end
@@ -4414,7 +4432,8 @@ let induction_without_atomization isrec with_evars elim names lid =
scheme.nargs + (if scheme.farg_in_concl then 1 else 0) in
if not (Int.equal (List.length lid) (scheme.nparams + nargs_indarg_farg))
then
- Tacticals.New.tclZEROMSG (msg_not_right_number_induction_arguments scheme)
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (msg_not_right_number_induction_arguments scheme)
else
let indvars,lid_params = List.chop nargs_indarg_farg lid in
(* terms to patternify we must patternify indarg or farg if present in concl *)
@@ -4528,7 +4547,8 @@ let guard_no_unifiable = Proofview.guard_no_unifiable >>= function
| Some l ->
Proofview.tclENV >>= function env ->
Proofview.tclEVARMAP >>= function sigma ->
- Proofview.tclZERO (RefinerError (env, sigma, UnresolvedBindings l))
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (RefinerError (env, sigma, UnresolvedBindings l))
let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
id ((pending,(c0,lbind)),(eqname,names)) t0 inhyps cls tac =
@@ -4831,7 +4851,9 @@ let reflexivity_red allowred =
let sigma = Tacmach.New.project gl in
let concl = maybe_betadeltaiota_concl allowred gl in
match match_with_equality_type env sigma concl with
- | None -> Proofview.tclZERO NoEquationFound
+ | None ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info NoEquationFound
| Some _ -> one_constructor 1 NoBindings
end
@@ -4873,8 +4895,9 @@ let match_with_equation c =
try
let res = match_with_equation env sigma c in
Proofview.tclUNIT res
- with NoEquationFound ->
- Proofview.tclZERO NoEquationFound
+ with NoEquationFound as exn ->
+ let _, info = Exninfo.capture exn in
+ Proofview.tclZERO ~info NoEquationFound
let symmetry_red allowred =
Proofview.Goal.enter begin fun gl ->
@@ -4987,7 +5010,9 @@ let transitivity_red allowred t =
| Some t -> Tacticals.New.pf_constr_of_global eq_data.trans >>= fun trans -> apply_list [trans; t])
| None,eq,eq_kind ->
match t with
- | None -> Tacticals.New.tclZEROMSG (str"etransitivity not supported for this relation.")
+ | None ->
+ let info = Exninfo.reify () in
+ Tacticals.New.tclZEROMSG ~info (str"etransitivity not supported for this relation.")
| Some t -> prove_transitivity eq eq_kind t
end
@@ -5005,8 +5030,8 @@ let transitivity t = transitivity_gen (Some t)
let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n)
let constr_eq ~strict x y =
- let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
- let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+ let fail ~info = Tacticals.New.tclFAIL ~info 0 (str "Not equal") in
+ let fail_universes ~info = Tacticals.New.tclFAIL ~info 0 (str "Not equal (due to universes)") in
Proofview.Goal.enter begin fun gl ->
let env = Tacmach.New.pf_env gl in
let evd = Tacmach.New.project gl in
@@ -5015,13 +5040,18 @@ let constr_eq ~strict x y =
let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
if strict then
if Evd.check_constraints evd csts then Proofview.tclUNIT ()
- else fail_universes
+ else
+ let info = Exninfo.reify () in
+ fail_universes ~info
else
(match Evd.add_constraints evd csts with
| evd -> Proofview.Unsafe.tclEVARS evd
- | exception Univ.UniverseInconsistency _ ->
- fail_universes)
- | None -> fail
+ | exception (Univ.UniverseInconsistency _ as e) ->
+ let _, info = Exninfo.capture e in
+ fail_universes ~info)
+ | None ->
+ let info = Exninfo.reify () in
+ fail ~info
end
let unify ?(state=TransparentState.full) x y =
@@ -5042,7 +5072,8 @@ let unify ?(state=TransparentState.full) x y =
let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
Proofview.Unsafe.tclEVARS sigma
with e when noncritical e ->
- Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
+ let e, info = Exninfo.capture e in
+ Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None)))
end
(** [tclWRAPFINALLY before tac finally] runs [before] before each
diff --git a/user-contrib/Ltac2/tac2match.ml b/user-contrib/Ltac2/tac2match.ml
index 22f65507c1..86c7b0e3be 100644
--- a/user-contrib/Ltac2/tac2match.ml
+++ b/user-contrib/Ltac2/tac2match.ml
@@ -131,7 +131,9 @@ module PatternMatching (E:StaticEnvironment) = struct
{ stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
(** Failure of the pattern-matching monad: no success. *)
- let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
+ let fail (type a) : a m = { stream = fun _ _ ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info matching_error }
let run (m : 'a m) =
let ctx = {
@@ -150,7 +152,11 @@ module PatternMatching (E:StaticEnvironment) = struct
let put_subst subst : unit m =
let s = { subst } in
- { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
+ { stream = fun k ctx -> match merge s ctx with
+ | None ->
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info matching_error
+ | Some s -> k () s }
(** {6 Pattern-matching} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:54:18 +0000