aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml38
-rw-r--r--plugins/funind/indfun_common.ml24
-rw-r--r--plugins/funind/recdef.ml13
-rw-r--r--plugins/ltac/evar_tactics.ml32
-rw-r--r--plugins/ltac/extraargs.mlg54
-rw-r--r--plugins/ltac/extraargs.mli4
-rw-r--r--plugins/ltac/extratactics.mlg8
-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/pptactic.ml2
-rw-r--r--plugins/ltac/taccoerce.ml7
-rw-r--r--plugins/ltac/tacintern.ml20
-rw-r--r--plugins/ltac/tacinterp.ml36
-rw-r--r--plugins/ltac/tacsubst.ml1
-rw-r--r--plugins/micromega/coq_micromega.ml4
-rw-r--r--plugins/setoid_ring/newring.ml32
-rw-r--r--plugins/ssr/ssrcommon.ml5
19 files changed, 212 insertions, 94 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/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f0457acd68..b864b18887 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -243,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type =
let new_ctxt, new_end_of_type =
decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
in
- let prove_new_hyp : tactic =
- tclTHEN
- (tclDO ctxt_size (Proofview.V82.of_tactic intro))
- (fun g ->
- let all_ids = pf_ids_of_hyps g in
- let new_ids, _ = list_chop ctxt_size all_ids in
- let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
- let evm, _ = pf_apply Typing.type_of g to_refine in
- tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g)
+ let prove_new_hyp =
+ let open Tacticals.New in
+ let open Tacmach.New in
+ tclTHEN (tclDO ctxt_size intro)
+ (Proofview.Goal.enter (fun g ->
+ let all_ids = pf_ids_of_hyps g in
+ let new_ids, _ = list_chop ctxt_size all_ids in
+ let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
+ let evm, _ =
+ Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+ to_refine
+ in
+ tclTHEN
+ (Proofview.Unsafe.tclEVARS evm)
+ (Proofview.V82.tactic (refine to_refine))))
in
let simpl_eq_tac =
change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
- prove_new_hyp
+ (Proofview.V82.of_tactic prove_new_hyp)
in
(* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *)
(* str "removing an equation " ++ fnl ()++ *)
@@ -534,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
let prov_hid = pf_get_new_id hid g in
let c = mkApp (mkVar hid, args) in
let evm, _ = pf_apply Typing.type_of g c in
- tclTHENLIST
- [ Refiner.tclEVARS evm
- ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c)
- ; thin [hid]
- ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ]
+ let open Tacticals.New in
+ Proofview.V82.of_tactic
+ (tclTHENLIST
+ [ Proofview.Unsafe.tclEVARS evm
+ ; pose_proof (Name prov_hid) c
+ ; clear [hid]
+ ; rename_hyp [(prov_hid, hid)] ])
g)
(fun (*
if not then we are in a mutual function block
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e83fe56cc9..af53f16e1f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,7 @@ open Names
open Pp
open Constr
open Libnames
-open Refiner
+open Tacmach
let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id)
let mk_rel_id = mk_prefix "R_"
@@ -395,7 +395,8 @@ let jmeq_refl () =
with e when CErrors.noncritical e -> raise (ToShow e)
let h_intros l =
- tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
+ Proofview.V82.of_tactic
+ (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l)
let h_id = Id.of_string "h"
let hrec_id = Id.of_string "hrec"
@@ -427,15 +428,16 @@ let evaluable_of_global_reference r =
| _ -> assert false
let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
- tclREPEAT
- (List.fold_right
- (fun (eq, b) i ->
- tclORELSE
- (Proofview.V82.of_tactic
- ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
- i)
- (if rev then List.rev eqs else eqs)
- (tclFAIL 0 (mt ())))
+ let open Tacticals in
+ (tclREPEAT
+ (List.fold_right
+ (fun (eq, b) i ->
+ tclORELSE
+ (Proofview.V82.of_tactic
+ ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
+ i)
+ (if rev then List.rev eqs else eqs)
+ (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"])
let decompose_lam_n sigma n =
if n < 0 then
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5c82ed38bb..9b2d9c4815 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g =
in
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
-let pf_type c tac gl =
- let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
- tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_type c tac =
+ let open Tacticals.New in
+ Proofview.Goal.enter (fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let evars, ty = Typing.type_of env sigma c in
+ tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty))
+
+let pf_type c tac =
+ Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty)))
let pf_typel l tac =
let rec aux tys l =
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/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4731e5c34..eb53fd45d0 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -31,6 +31,8 @@ let create_generic_quotation name e wit =
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
+let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global
+
let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
@@ -342,3 +344,55 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon }
| [ local_test_lpar_id_colon(x) ] -> { () }
END
+
+{
+
+(* Work around a limitation of the macro system *)
+let strategy_level0 = Pcoq.Prim.strategy_level
+
+let pr_strategy _ _ _ v = Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy }
+| [ strategy_level0(n) ] -> { n }
+END
+
+{
+
+let intern_strategy ist v = match v with
+| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id)
+| ArgArg v -> ArgArg v
+
+let subst_strategy _ v = v
+
+let interp_strategy ist gl = function
+| ArgArg n -> gl.Evd.sigma, n
+| ArgVar { CAst.v = id; CAst.loc } ->
+ let v =
+ try Id.Map.find id ist.lfun
+ with Not_found ->
+ CErrors.user_err ?loc
+ (str "Unbound variable " ++ Id.print id ++ str".")
+ in
+ let v =
+ try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v
+ with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level"
+ in
+ gl.Evd.sigma, v
+
+let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level_or_var
+ TYPED AS strategy_level
+ PRINTED BY { pr_strategy }
+ INTERPRETED BY { interp_strategy }
+ GLOBALIZED BY { intern_strategy }
+ SUBSTITUTED BY { subst_strategy }
+ RAW_PRINTED BY { pr_loc_strategy }
+ GLOB_PRINTED BY { pr_loc_strategy }
+| [ strategy_level(n) ] -> { ArgArg n }
+| [ identref(id) ] -> { ArgVar id }
+END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index fbdb7c0032..e52bf55f71 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -78,3 +78,7 @@ val wit_in_clause :
(lident Locus.clause_expr,
lident Locus.clause_expr,
Id.t Locus.clause_expr) Genarg.genarg_type
+
+val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type
+
+val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0bad3cbe5b..ffb597d4cb 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP =
TACTIC EXTEND optimize_heap
| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP }
END
+
+(** Tactic analogous to [Strategy] vernacular *)
+
+TACTIC EXTEND with_strategy
+| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> {
+ with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac)
+}
+END
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/pptactic.ml b/plugins/ltac/pptactic.ml
index 09f1fc371a..d74e981c6d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1325,6 +1325,8 @@ let () =
register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
register_basic_print0 wit_ref
pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
+ register_basic_print0 wit_smart_global
+ (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
register_basic_print0 wit_ident pr_id pr_id pr_id;
register_basic_print0 wit_var pr_lident pr_lident pr_id;
register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 04d85ed390..91d26519b8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v =
| VarRef var -> EvalVarRef var
| ConstRef c -> EvalConstRef c
| IndRef _ | ConstructRef _ -> fail ()
+ else if has_type v (topwit wit_smart_global) then
+ let open GlobRef in
+ let r = out_gen (topwit wit_smart_global) v in
+ match r with
+ | VarRef var -> EvalVarRef var
+ | ConstRef c -> EvalConstRef c
+ | IndRef _ | ConstructRef _ -> fail ()
else
match Value.to_constr v with
| Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 597c3fdaac..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
@@ -305,6 +312,12 @@ let intern_evaluable_reference_or_by_notation ist = function
(Notation.interp_notation_as_global_reference ?loc
GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+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
+ GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
+
(* Globalize a reduction expression *)
let intern_evaluable ist r =
let f ist r =
@@ -813,6 +826,7 @@ let intern_ltac ist tac =
let () =
Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+ Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
Genintern.register_intern0 wit_ident intern_ident';
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6debc7d9b9..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) ->
@@ -2022,6 +2033,7 @@ let interp_pre_ident ist env sigma s =
let () =
register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+ register_interp0 wit_smart_global (lift interp_reference);
register_interp0 wit_ref (lift interp_reference);
register_interp0 wit_pre_ident (lift interp_pre_ident);
register_interp0 wit_ident (lift interp_ident);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 600c30b403..ed298b7e66 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
let () =
Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
Genintern.register_subst0 wit_ref subst_global_reference;
+ Genintern.register_subst0 wit_smart_global subst_global_reference;
Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
Genintern.register_subst0 wit_ident (fun _ v -> v);
Genintern.register_subst0 wit_var (fun _ v -> v);
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ee2c87d19a..0f8d941b41 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1897,8 +1897,6 @@ type provername = string * int option
* The caching mechanism.
*)
-open Persistent_cache
-
module MakeCache (T : sig
type prover_option
type coeff
@@ -1922,7 +1920,7 @@ struct
Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0)
end
- include PHashtable (E)
+ include Persistent_cache.PHashtable (E)
let memo_opt use_cache cache_file f =
let memof = memo cache_file f in
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
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 62d4adca43..01e8daf82d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -22,7 +22,7 @@ open Locusops
open Ltac_plugin
open Tacmach
-open Refiner
+open Tacticals
open Libnames
open Ssrmatching_plugin
open Ssrmatching
@@ -81,6 +81,9 @@ let nohint = false, []
type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma
+let project gl = gl.Evd.sigma
+let re_sig it sigma = { Evd.it = it; Evd.sigma = sigma }
+
let push_ctx a gl = re_sig (sig_it gl, a) (project gl)
let push_ctxs a gl =
re_sig (List.map (fun x -> x,a) (sig_it gl)) (project gl)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 14:48:23 +0000