aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/ltac/g_class.mlg15
-rw-r--r--plugins/ltac/g_ltac.mlg4
-rw-r--r--plugins/ltac/g_tactic.mlg3
-rw-r--r--plugins/ltac/tacinterp.ml33
-rw-r--r--plugins/setoid_ring/newring.ml32
6 files changed, 49 insertions, 42 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 0c305d09e8..c485c38009 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -290,7 +290,6 @@ let constr_of_term c = EConstr.of_constr (constr_of_term c)
let rec proof_tac p : unit Proofview.tactic =
Proofview.Goal.enter begin fun gl ->
- try (* type_of can raise exceptions *)
match p.p_rule with
Ax c -> exact_check (EConstr.of_constr c)
| SymAx c ->
@@ -350,7 +349,6 @@ let rec proof_tac p : unit Proofview.tactic =
app_global_with_holes _f_equal [|intype;outtype;proj;ti;tj|] 1 in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tacticals.New.tclTHEN injt (proof_tac prf))))
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
end
let refute_tac c t1 t2 p =
@@ -508,11 +506,9 @@ let f_equal =
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
let cut_eq c1 c2 =
- try (* type_of can raise an exception *)
Tacticals.New.tclTHENS
(mk_eq _eq c1 c2 Tactics.cut)
[Proofview.tclUNIT ();Tacticals.New.tclTRY ((app_global _refl_equal [||]) apply)]
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
in
Proofview.tclORELSE
begin match EConstr.kind sigma concl with
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 0f0341f123..81e745b714 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
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/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 5ae0b2efd7..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 ->
@@ -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) ->
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 633cdbd735..e7c75e029e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -690,15 +690,13 @@ let ring_lookup (f : Value.t) lH rl t =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- try (* find_ring_strucure can raise an exception *)
- let rl = make_args_list sigma rl t in
- let evdref = ref sigma in
- let e = find_ring_structure env sigma rl in
- let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
- let lH = carg (make_hyp_list env evdref lH) in
- let ring = ltac_ring_structure e in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ let rl = make_args_list sigma rl t in
+ let evdref = ref sigma in
+ let e = find_ring_structure env sigma rl in
+ let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.ring_carrier) rl) in
+ let lH = carg (make_hyp_list env evdref lH) in
+ let ring = ltac_ring_structure e in
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (ring@[lH;rl]))
end
(***********************************************************************)
@@ -984,13 +982,11 @@ let field_lookup (f : Value.t) lH rl t =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- try
- let rl = make_args_list sigma rl t in
- let evdref = ref sigma in
- let e = find_field_structure env sigma rl in
- let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
- let lH = carg (make_hyp_list env evdref lH) in
- let field = ltac_field_structure e in
- Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ let rl = make_args_list sigma rl t in
+ let evdref = ref sigma in
+ let e = find_field_structure env sigma rl in
+ let rl = Value.of_constr (make_term_list env evdref (EConstr.of_constr e.field_carrier) rl) in
+ let lH = carg (make_hyp_list env evdref lH) in
+ let field = ltac_field_structure e in
+ Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) (Value.apply f (field@[lH;rl]))
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 01:03:43 +0000