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/extraargs.mlg54
-rw-r--r--plugins/ltac/extraargs.mli4
-rw-r--r--plugins/ltac/extratactics.mlg8
-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.ml3
-rw-r--r--plugins/ltac/tacsubst.ml1
9 files changed, 112 insertions, 19 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/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/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 1a2011b960..6d350ade8d 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1098,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
@@ -2033,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);
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 04:59:20 +0000