aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-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
6 files changed, 85 insertions, 39 deletions
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 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:13:52 +0000