aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml32
-rw-r--r--plugins/ltac/tacintern.ml13
-rw-r--r--plugins/ltac/tacinterp.ml35
3 files changed, 50 insertions, 30 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 17a7121a3f..f867a47c08 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -14,10 +14,7 @@ open Constr
open Context
open CErrors
open Evar_refiner
-open Tacmach
open Tacexpr
-open Refiner
-open Evd
open Locus
open Context.Named.Declaration
open Ltac_pretype
@@ -26,7 +23,11 @@ module NamedDecl = Context.Named.Declaration
(* The instantiate tactic *)
-let instantiate_evar evk (ist,rawc) env sigma =
+let instantiate_evar evk (ist,rawc) =
+ let open Proofview.Notations in
+ Proofview.tclENV >>= fun env ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
let evi = Evd.find sigma evk in
let filtered = Evd.evar_filtered_env env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
@@ -37,7 +38,8 @@ let instantiate_evar evk (ist,rawc) env sigma =
ltac_genargs = ist.Geninterp.lfun;
} in
let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
- tclEVARS sigma'
+ Proofview.Unsafe.tclEVARS sigma'
+ end
let evar_list sigma c =
let rec evrec acc c =
@@ -47,14 +49,15 @@ let evar_list sigma c =
evrec [] c
let instantiate_tac n c ido =
- Proofview.V82.tactic begin fun gl ->
- let env = Global.env () in
- let sigma = gl.sigma in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
let evl =
match ido with
- ConclLocation () -> evar_list sigma (pf_concl gl)
+ ConclLocation () -> evar_list sigma concl
| HypLocation (id,hloc) ->
- let decl = Environ.lookup_named id (pf_env gl) in
+ let decl = Environ.lookup_named id env in
match hloc with
InHyp ->
(match decl with
@@ -70,17 +73,16 @@ let instantiate_tac n c ido =
user_err Pp.(str "Not enough uninstantiated existential variables.");
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
- instantiate_evar evk c env sigma gl
+ instantiate_evar evk c
end
let instantiate_tac_by_name id c =
- Proofview.V82.tactic begin fun gl ->
- let env = Global.env () in
- let sigma = gl.sigma in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
let evk =
try Evd.evar_key id sigma
with Not_found -> user_err Pp.(str "Unknown existential variable.") in
- instantiate_evar evk c env sigma gl
+ instantiate_evar evk c
end
let let_evar name typ =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 929fd5e132..1aa3af0087 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -95,9 +95,16 @@ 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
- try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
- with Not_found -> Nametab.error_global_not_found 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 match locate_global_with_alias qid with
+ | r -> ArgArg (qid.CAst.loc, r)
+ | exception Not_found ->
+ if not !strict_check && qualid_is_ident qid then
+ let id = qualid_basename qid in
+ ArgArg (qid.CAst.loc, GlobRef.VarRef id)
+ else Nametab.error_global_not_found qid
let intern_ltac_variable ist qid =
if qualid_is_ident qid && find_var (qualid_basename qid) ist then
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d1f031b418..6d350ade8d 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))
@@ -535,9 +545,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
@@ -1059,7 +1070,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 ->
@@ -1087,7 +1098,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacShowHyps tac ->
Proofview.V82.tactic begin
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
- end
+ end [@ocaml.warning "-3"]
| TacAbstract (t,ido) ->
let call = LtacMLCall tac in
let trace = push_trace(None,call) ist in
@@ -1149,7 +1160,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) ->
@@ -1175,7 +1186,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
@@ -1278,7 +1289,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) ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:27:06 +0000