aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_auto.mlg50
-rw-r--r--plugins/ltac/g_tactic.mlg15
-rw-r--r--plugins/ltac/rewrite.ml19
3 files changed, 65 insertions, 19 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 44472a1995..7e8400910c 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -116,12 +116,25 @@ END
let make_depth n = snd (Eauto.make_dimension n None)
+(* deprecated in 8.13; the second int_or_var will be removed *)
+let deprecated_eauto_bfs =
+ CWarnings.create
+ ~name:"eauto_bfs" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.")
+
+let deprecated_bfs tacname =
+ CWarnings.create
+ ~name:"eauto_bfs" ~category:"deprecated"
+ (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.")
+
}
TACTIC EXTEND eauto
| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+ {
+ ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () );
+ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND new_eauto
@@ -135,13 +148,17 @@ END
TACTIC EXTEND debug_eauto
| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+ {
+ ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () );
+ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND info_eauto
| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
hintbases(db) ] ->
- { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
+ {
+ ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () );
+ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db }
END
TACTIC EXTEND dfs_eauto
@@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto
{ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db }
END
+TACTIC EXTEND bfs_eauto
+| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems)
+ hintbases(db) ] ->
+ { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db }
+END
+
TACTIC EXTEND autounfold
| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl }
END
@@ -240,10 +263,21 @@ ARGUMENT EXTEND opthints
END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
- let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in
- Hints.add_hints ~locality
- (match dbnames with None -> ["core"] | Some l -> l) entry;
+| #[ locality = Attributes.option_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
+ let open Goptions in
+ let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
+ let () = match locality with
+ | OptGlobal ->
+ if Global.sections_are_opened () then
+ CErrors.user_err Pp.(str
+ "This command does not support the global attribute in sections.");
+ | OptExport ->
+ if Global.sections_are_opened () then
+ CErrors.user_err Pp.(str
+ "This command does not support the export attribute in sections.");
+ | OptDefault | OptLocal -> ()
+ in
+ Hints.add_hints ~locality
+ (match dbnames with None -> ["core"] | Some l -> l) entry;
}
END
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index ecfe6c1664..072206c39c 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -234,9 +234,7 @@ GRAMMAR EXTEND Gram
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
- | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
- (* have used int_or_var instead of nat_or_var for compatibility *)
- { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
+ | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ]
;
occs:
[ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
@@ -379,9 +377,11 @@ GRAMMAR EXTEND Gram
{ {onhyps=None; concl_occs=occs} }
| "*"; "|-"; occs=concl_occ ->
{ {onhyps=None; concl_occs=occs} }
- | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
+ | "|-"; occs=concl_occ ->
+ { {onhyps=Some []; concl_occs=occs} }
+ | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ ->
{ {onhyps=Some hl; concl_occs=occs} }
- | hl=LIST0 hypident_occ SEP"," ->
+ | hl = LIST1 hypident_occ SEP "," ->
{ {onhyps=Some hl; concl_occs=NoOccurrences} } ] ]
;
clause_dft_concl:
@@ -450,6 +450,11 @@ GRAMMAR EXTEND Gram
;
as_or_and_ipat:
[ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat }
+ | "as"; ipat = equality_intropattern ->
+ { match ipat with
+ | IntroRewrite _ -> user_err Pp.(str "Disjunctive/conjunctive pattern expected.")
+ | IntroInjection _ -> user_err Pp.(strbrk "Found an injection pattern while a disjunctive/conjunctive pattern was expected; use " ++ str "\"injection as pattern\"" ++ strbrk " instead.")
+ | _ -> assert false }
| -> { None } ] ]
;
eqn_ipat:
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 26e2b18a02..77162ce89a 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -13,7 +13,6 @@ open CErrors
open Util
open Names
open Nameops
-open Namegen
open Constr
open Context
open EConstr
@@ -485,7 +484,7 @@ let rec decompose_app_rel env evd t =
let (f', argl, argr) = decompose_app_rel env evd arg in
let ty = Retyping.get_type_of env evd argl in
let r = Retyping.relevance_of_type env evd ty in
- let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
+ let f'' = mkLambda (make_annot (Name Namegen.default_dependent_ident) r, ty,
mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
in (f'', argl, argr)
@@ -1119,7 +1118,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
*)
| Lambda (n, t, b) when flags.under_lambdas ->
- let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
+ let unfresh, n' =
+ let id = match n.binder_name with
+ | Anonymous -> Namegen.default_dependent_ident
+ | Name id -> id
+ in
+ let id = Tactics.fresh_id_in_env unfresh id env in
+ Id.Set.add id unfresh, {n with binder_name = Name id}
+ in
let unfresh = match n'.binder_name with
| Anonymous -> unfresh
| Name id -> Id.Set.add id unfresh
@@ -1542,7 +1548,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
(* For compatibility *)
let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in
let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in
- let treat sigma res =
+ let treat sigma res state =
match res with
| None -> newfail 0 (str "Nothing to rewrite")
| Some None ->
@@ -1553,7 +1559,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
let (undef, prf, newt) = res in
let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in
let gls = List.rev (Evd.fold_undefined fold undef []) in
- let gls = List.map Proofview.with_empty_state gls in
+ let gls = List.map (fun gl -> Proofview.goal_with_state gl state) gls in
match clause, prf with
| Some id, Some p ->
let tac = tclTHENLIST [
@@ -1583,6 +1589,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
+ let state = Proofview.Goal.state gl in
let sigma = Tacmach.New.project gl in
let ty = match clause with
| None -> concl
@@ -1602,7 +1609,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
in
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
- treat sigma res <*>
+ treat sigma res state <*>
(* For compatibility *)
beta <*> Proofview.shelve_unifiable
with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 03:56:03 +0000