aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_class.mlg19
-rw-r--r--plugins/ltac/g_ltac.mlg4
-rw-r--r--plugins/ltac/g_tactic.mlg3
-rw-r--r--plugins/ltac/rewrite.ml44
-rw-r--r--plugins/ltac/tacintern.ml103
-rw-r--r--plugins/ltac/tacinterp.ml112
-rw-r--r--plugins/ltac/tactic_matching.ml10
7 files changed, 185 insertions, 110 deletions
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 0f0341f123..35c90444b1 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -54,16 +54,23 @@ END
{
+let pr_search_strategy_name _prc _prlc _prt = function
+ | Dfs -> Pp.str "dfs"
+ | Bfs -> Pp.str "bfs"
+
let pr_search_strategy _prc _prlc _prt = function
- | Some Dfs -> Pp.str "dfs"
- | Some Bfs -> Pp.str "bfs"
+ | Some s -> pr_search_strategy_name _prc _prlc _prt s
| None -> Pp.mt ()
}
+ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name }
+| [ "bfs" ] -> { Bfs }
+| [ "dfs" ] -> { Dfs }
+END
+
ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
-| [ "(bfs)" ] -> { Some Bfs }
-| [ "(dfs)" ] -> { Some Dfs }
+| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s }
| [ ] -> { None }
END
@@ -135,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/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index aef5f645f4..0e661543db 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram
;
match_key:
[ [ "match" -> { Once }
- | "lazymatch" -> { Select }
- | "multimatch" -> { General } ] ]
+ | IDENT "lazymatch" -> { Select }
+ | IDENT "multimatch" -> { General } ] ]
;
input_fun:
[ [ "_" -> { Name.Anonymous }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 6a158bde17..e51b1f051d 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -30,9 +30,6 @@ open Pcoq
let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
-let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter CLexer.add_keyword tactic_kw
-
let err () = raise Stream.Failure
(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3b8fb48eb0..4bc8d61258 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite."
let rec decompose_app_rel env evd t =
(* Head normalize for compatibility with the old meta mechanism *)
- let t = Reductionops.whd_betaiota evd t in
+ let t = Reductionops.whd_betaiota env evd t in
match EConstr.kind evd t with
| App (f, [||]) -> assert false
| App (f, [|arg|]) ->
@@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
~fail:true env sigma in
let evd = solve_remaining_by env sigma holes by in
- let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
+ let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in
let c1 = nf c1 and c2 = nf c2
and rew_car = nf car and rel = nf rel
and prf = nf prf in
@@ -971,7 +971,7 @@ let unfold_match env sigma sk app =
| App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
- Reductionops.whd_beta sigma (mkApp (v, args))
+ Reductionops.whd_beta env sigma (mkApp (v, args))
| _ -> app
let is_rew_cast = function RewCast _ -> true | _ -> false
@@ -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/tacintern.ml b/plugins/ltac/tacintern.ml
index 929fd5e132..bcfdb5318e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -14,7 +14,6 @@ open CAst
open Pattern
open Genredexpr
open Glob_term
-open Tacred
open Util
open Names
open Libnames
@@ -95,9 +94,22 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s)
let intern_global_reference ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
+ else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
+ let id = qualid_basename qid in
+ ArgArg (qid.CAst.loc, GlobRef.VarRef id)
else
- try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
- with Not_found -> Nametab.error_global_not_found qid
+ let r =
+ try locate_global_with_alias ~head:true qid
+ with
+ | Not_found as exn ->
+ if not !strict_check && qualid_is_ident qid then
+ let id = qualid_basename qid in
+ GlobRef.VarRef id
+ else
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
+ in
+ ArgArg (qid.CAst.loc, r)
let intern_ltac_variable ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
@@ -142,9 +154,10 @@ let intern_isolated_tactic_reference strict ist qid =
with Not_found ->
(* Tolerance for compatibility, allow not to use "constr:" *)
try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid))
- with Not_found ->
- (* Reference not found *)
- Nametab.error_global_not_found qid
+ with Not_found as exn ->
+ (* Reference not found *)
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
(* Internalize an applied tactic reference *)
@@ -161,9 +174,10 @@ let intern_applied_tactic_reference ist qid =
with Not_found ->
(* A global tactic *)
try intern_applied_global_tactic_reference qid
- with Not_found ->
- (* Reference not found *)
- Nametab.error_global_not_found qid
+ with Not_found as exn ->
+ (* Reference not found *)
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
(* Intern a reference parsed in a non-tactic entry *)
@@ -176,7 +190,7 @@ let intern_non_tactic_reference strict ist qid =
with Not_found ->
(* Tolerance for compatibility, allow not to use "ltac:" *)
try intern_isolated_global_tactic_reference qid
- with Not_found ->
+ with Not_found as exn ->
(* By convention, use IntroIdentifier for unbound ident, when not in a def *)
if qualid_is_ident qid && not strict then
let id = qualid_basename qid in
@@ -184,7 +198,8 @@ let intern_non_tactic_reference strict ist qid =
TacGeneric ipat
else
(* Reference not found *)
- Nametab.error_global_not_found qid
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
let intern_message_token ist = function
| (MsgString _ | MsgInt _ as x) -> x
@@ -287,45 +302,43 @@ let intern_destruction_arg ist = function
else
clear,ElimOnIdent (make ?loc id)
-let short_name = function
- | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+let short_name qid =
+ if qualid_is_ident qid && not !strict_check then
Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- | _ -> None
-
-let intern_evaluable_global_reference ist qid =
- try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
- with Not_found ->
- if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
- else Nametab.error_global_not_found qid
-
-let intern_evaluable_reference_or_by_notation ist = function
- | {v=AN r} -> intern_evaluable_global_reference ist r
+ else None
+
+let evalref_of_globref ?loc ?short = function
+ | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
+ | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+ | r ->
+ let tpe = match r with
+ | GlobRef.IndRef _ -> "inductive"
+ | GlobRef.ConstructRef _ -> "constructor"
+ | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false
+ in
+ user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++
+ Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+ str "into an evaluable reference.")
+
+let intern_evaluable ist = function
+ | {v=AN qid} ->
+ begin match intern_global_reference ist qid with
+ | ArgVar _ as v -> v
+ | ArgArg (loc, r) ->
+ let short = short_name qid in
+ evalref_of_globref ?loc ?short r
+ end
| {v=ByNotation (ntn,sc);loc} ->
- evaluable_of_global_reference ist.genv
- (Notation.interp_notation_as_global_reference ?loc
- GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+ let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
+ let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
+ evalref_of_globref ?loc r
let intern_smart_global ist = function
| {v=AN r} -> intern_global_reference ist r
| {v=ByNotation (ntn,sc);loc} ->
- ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+ ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true
GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
-(* Globalize a reduction expression *)
-let intern_evaluable ist r =
- let f ist r =
- let e = intern_evaluable_reference_or_by_notation ist r in
- let na = short_name r in
- ArgArg (e,na)
- in
- match r with
- | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
- ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
- | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
- let id = qualid_basename qid in
- ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
- | _ -> f ist r
-
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
let intern_flag ist red =
@@ -386,10 +399,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let c = Constrintern.interp_reference sign r in
match DAst.get c with
| GRef (r,None) ->
- Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+ Inl (evalref_of_globref r)
| GVar id ->
- let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
- Inl (ArgArg (r,None))
+ let r = evalref_of_globref (GlobRef.VarRef id) in
+ Inl r
| _ ->
let bound_names = Glob_ops.bound_glob_vars c in
Inr (bound_names,(c,None),dummy_pat) in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5ae0b2efd7..97f7a198e6 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -162,17 +162,27 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let catch_error call_trace f x =
+let update_loc ?loc (e, info) =
+ (e, Option.cata (Loc.add_loc info) info loc)
+
+let catch_error ?loc call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
+ let e = update_loc ?loc e in
catching_error call_trace Exninfo.iraise e
-let wrap_error tac k =
- if is_traced () then Proofview.tclORELSE tac k else tac
+let catch_error_loc ?loc tac =
+ Proofview.tclOR tac (fun exn ->
+ let (e, info) = update_loc ?loc exn in
+ Proofview.tclZERO ~info e)
+
+let wrap_error ?loc tac k =
+ if is_traced () then Proofview.tclORELSE tac k
+ else catch_error_loc ?loc tac
-let catch_error_tac call_trace tac =
- wrap_error
+let catch_error_tac ?loc call_trace tac =
+ wrap_error ?loc
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -368,7 +378,9 @@ let interp_reference ist env sigma = function
with Not_found ->
try
GlobRef.VarRef (get_id (Environ.lookup_named id env))
- with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)
let try_interp_evaluable env (loc, id) =
let v = Environ.lookup_named id env in
@@ -381,17 +393,21 @@ let interp_evaluable ist env sigma = function
(* Maybe [id] has been introduced by Intro-like tactics *)
begin
try try_interp_evaluable env (loc, id)
- with Not_found ->
+ with Not_found as exn ->
match r with
| EvalConstRef _ -> r
- | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
+ | _ ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)
end
| ArgArg (r,None) -> r
| ArgVar {loc;v=id} ->
try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id)
with Not_found ->
try try_interp_evaluable env (loc, id)
- with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id)
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info (qualid_of_ident ?loc id)
(* Interprets an hypothesis name *)
let interp_occurrences ist occs =
@@ -535,9 +551,10 @@ let interp_gen kind ist pattern_mode flags env sigma c =
ltac_idents = constrvars.idents;
ltac_genargs = ist.lfun;
} in
- let trace = push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist in
+ let loc = loc_of_glob_constr term in
+ let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error trace (understand_ltac flags env sigma vars kind) term
+ catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -652,8 +669,9 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
let c = coerce_to_closed_constr env x in
Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id)
- with Not_found ->
- Nametab.error_global_not_found (qualid_of_ident ?loc id))
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info (qualid_of_ident ?loc id))
| Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b)
| Inr c -> Inr (interp_typed_pattern ist env sigma c) in
interp_occurrences ist occs, p
@@ -763,7 +781,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 =
@@ -1059,7 +1079,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac trace (interp_atomic ist t))
+ (catch_error_tac ?loc trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1076,11 +1096,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)
@@ -1149,7 +1173,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
; poly
; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (tactic_of_value ist v)
+ Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1163,8 +1187,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 ())
@@ -1175,7 +1202,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
in
Ftactic.run args tac
@@ -1256,7 +1283,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
@@ -1278,7 +1305,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1302,12 +1329,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 =
@@ -1335,7 +1368,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
@@ -1353,11 +1387,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 =
@@ -1551,10 +1589,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 23:03:59 +0000