aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md4
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg6
-rw-r--r--plugins/ltac/pptactic.ml11
-rw-r--r--plugins/ltac/tacentries.ml8
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml6
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--plugins/setoid_ring/newring.ml6
-rw-r--r--plugins/ssr/ssrparser.mlg8
-rw-r--r--test-suite/output/bug_13004.out2
-rw-r--r--test-suite/output/bug_13004.v7
-rw-r--r--test-suite/output/print_ltac.out2
-rw-r--r--user-contrib/Ltac2/tac2core.ml2
16 files changed, 43 insertions, 29 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ae4c6328b5..7d2100515d 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,9 @@
## Changes between Coq 8.12 and Coq 8.13
+- Tactic language: TacGeneric now takes an argument to tell if it
+ comes from a notation. Use `None` if not and `Some foo` to tell to
+ print such TacGeneric surrounded with `foo:( )`.
+
## Changes between Coq 8.11 and Coq 8.12
### Code formatting
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index eb53fd45d0..863c4d37d8 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -25,7 +25,7 @@ open Locus
(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
let create_generic_quotation name e wit =
- let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
+ let inject (loc, v) = Tacexpr.TacGeneric (Some name, Genarg.in_gen (Genarg.rawwit wit) v) in
Tacentries.create_ltac_quotation name inject (e, None)
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 78cde2cde8..d88cda177e 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -180,7 +180,7 @@ GRAMMAR EXTEND Gram
[ [ a = tactic_arg -> { a }
| c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
(* Unambiguous entries: tolerated w/o "ltac:" modifier *)
- | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
+ | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
(* Can be used as argument and at toplevel in tactic expressions. *)
tactic_arg:
@@ -209,9 +209,9 @@ GRAMMAR EXTEND Gram
| c = Constr.constr -> { ConstrTerm c } ] ]
;
tactic_atom:
- [ [ n = integer -> { TacGeneric (genarg_of_int n) }
+ [ [ n = integer -> { TacGeneric (None, genarg_of_int n) }
| r = reference -> { TacCall (CAst.make ~loc (r,[])) }
- | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
+ | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
match_key:
[ [ "match" -> { Once }
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index f69fe064a7..85bb901046 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -338,8 +338,8 @@ let string_of_genarg_arg (ArgumentType arg) =
| Extend.Uentryl (_, l) -> prtac LevelSome arg
| _ ->
match arg with
- | TacGeneric arg ->
- let pr l arg = prtac l (TacGeneric arg) in
+ | TacGeneric (isquot,arg) ->
+ let pr l arg = prtac l (TacGeneric (isquot,arg)) in
pr_any_arg pr symb arg
| _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
@@ -571,7 +571,7 @@ let pr_goal_selector ~toplevel s =
let pr_let_clause k pr_gen pr_arg (na,(bl,t)) =
let pr = function
- | TacGeneric arg ->
+ | TacGeneric (_,arg) ->
let name = string_of_genarg_arg (genarg_tag arg) in
if name = "unit" || name = "int" then
(* Hard-wired parsing rules *)
@@ -1049,8 +1049,9 @@ let pr_goal_selector ~toplevel s =
pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
| TacArg { CAst.v=TacFreshId l } ->
primitive "fresh" ++ pr_fresh_ids l, latom
- | TacArg { CAst.v=TacGeneric arg } ->
- pr.pr_generic env sigma arg, latom
+ | TacArg { CAst.v=TacGeneric (isquot,arg) } ->
+ let p = pr.pr_generic env sigma arg in
+ (match isquot with Some name -> str name ++ str ":(" ++ p ++ str ")" | None -> p), latom
| TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
pr.pr_reference f, latom
| TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f8c25d5dd0..fcd60ea250 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -174,7 +174,7 @@ let add_tactic_entry (kn, ml, tg) state =
if Genarg.has_type arg wit && not ml then
Tacexp (Genarg.out_gen wit arg)
else
- TacGeneric arg
+ TacGeneric (None, arg)
in
let l = List.map map l in
(TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr)
@@ -349,7 +349,7 @@ let extend_atomic_tactic name entries =
| TacNonTerm (_, (symb, _)) ->
let EntryName (typ, e) = prod_item_of_symbol 0 symb in
let Genarg.Rawwit wit = typ in
- let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in
+ let inj x = TacArg (CAst.make @@ TacGeneric (None, Genarg.in_gen typ x)) in
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
@@ -780,7 +780,7 @@ let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
let len = ml_sig_len sign in
let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
- let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
+ let body = TacGeneric (None, in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
let vars = List.map (fun id -> Name id) vars in
let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
let id = Names.Id.of_string name in
@@ -876,7 +876,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
let (rpr, gpr, tpr) = arg.arg_printer in
let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in
let () = create_ltac_quotation name
- (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v))
+ (fun (loc, v) -> Tacexpr.TacGeneric (Some name,Genarg.in_gen (Genarg.rawwit wit) v))
(entry, None)
in
(wit, entry)
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index b261096b63..eaedf8d9c1 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -154,7 +154,7 @@ constraint 'a = <
(** Possible arguments of a tactic definition *)
type 'a gen_tactic_arg =
- | TacGeneric of 'lev generic_argument
+ | TacGeneric of string option * 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 650349b586..50767821e4 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -153,7 +153,7 @@ constraint 'a = <
(** Possible arguments of a tactic definition *)
type 'a gen_tactic_arg =
- | TacGeneric of 'lev generic_argument
+ | TacGeneric of string option * 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index afa79a88db..dea216045e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -195,7 +195,7 @@ let intern_non_tactic_reference strict ist qid =
if qualid_is_ident qid && not strict then
let id = qualid_basename qid in
let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in
- TacGeneric ipat
+ TacGeneric (None,ipat)
else
(* Reference not found *)
let _, info = Exninfo.capture exn in
@@ -713,9 +713,9 @@ and intern_tacarg strict onlytac ist = function
| TacPretype c -> TacPretype (intern_constr ist c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (intern_tactic onlytac ist t)
- | TacGeneric arg ->
+ | TacGeneric (isquot,arg) ->
let arg = intern_genarg ist arg in
- TacGeneric arg
+ TacGeneric (isquot,arg)
(* Reads the rules of a Match Context or a Match *)
and intern_match_rule onlytac ist ?(as_type=false) = function
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2258201c22..ffc8a81994 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1247,7 +1247,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
- | TacGeneric arg -> interp_genarg ist arg
+ | TacGeneric (_,arg) -> interp_genarg ist arg
| Reference r -> interp_ltac_reference false ist r
| ConstrMayEval c ->
Ftactic.enter begin fun gl ->
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index c2f1589b74..fd869b225f 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -237,7 +237,7 @@ and subst_tacarg subst = function
| TacPretype c -> TacPretype (subst_glob_constr subst c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (subst_tactic subst t)
- | TacGeneric arg -> TacGeneric (subst_genarg subst arg)
+ | TacGeneric (isquot,arg) -> TacGeneric (isquot,subst_genarg subst arg)
(* Reads the rules of a Match Context or a Match *)
and subst_match_rule subst = function
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6ed6b8da91..5f5a974b6a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -127,8 +127,8 @@ let closed_term_ast =
let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
TacFun([Name(Id.of_string"t")],
TacML(CAst.make (tacname,
- [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
- TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
+ [TacGeneric (None, Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
+ TacGeneric (None, Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
(*
let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
*)
@@ -200,7 +200,7 @@ let exec_tactic env evd n f args =
(* Build the getter *)
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in
- let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in
+ let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in
let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in
(* Evaluate the whole result *)
let gl = dummy_goal env evd in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 98439e27a1..b32b58062a 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -1682,7 +1682,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (*
let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args))
let tclintros_expr ?loc tac ipats =
- let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
+ let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in
ssrtac_expr ?loc "tclintros" args
}
@@ -1777,7 +1777,7 @@ let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"]
let ssrdotac_expr ?loc n m tac clauses =
let arg = ((n, m), tac), clauses in
- ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)]
+ ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)]
}
@@ -1828,7 +1828,7 @@ let tclseq_expr ?loc tac dir arg =
let arg1 = in_gen (rawwit wit_ssrtclarg) tac in
let arg2 = in_gen (rawwit wit_ssrseqdir) dir in
let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in
- ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3])
+ ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3])
}
@@ -2451,7 +2451,7 @@ GRAMMAR EXTEND Gram
tactic_expr: LEVEL "3"
[ RIGHTA [ IDENT "abstract"; gens = ssrdgens ->
{ ssrtac_expr ~loc "abstract"
- [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
+ [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]];
END
TACTIC EXTEND ssrabstract
| [ "abstract" ssrdgens(gens) ] -> {
diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out
new file mode 100644
index 0000000000..2bd7d67535
--- /dev/null
+++ b/test-suite/output/bug_13004.out
@@ -0,0 +1,2 @@
+Ltac bug_13004.t := ltac2:(print (of_string "hi"))
+Ltac bug_13004.u := ident:(H)
diff --git a/test-suite/output/bug_13004.v b/test-suite/output/bug_13004.v
new file mode 100644
index 0000000000..bf4a8285d0
--- /dev/null
+++ b/test-suite/output/bug_13004.v
@@ -0,0 +1,7 @@
+Require Import Ltac2.Ltac2 Ltac2.Message.
+
+Ltac t := ltac2:(print (of_string "hi")).
+Ltac u := ident:(H).
+
+Print t.
+Print u.
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
index 58931c4b82..5f88ec2e41 100644
--- a/test-suite/output/print_ltac.out
+++ b/test-suite/output/print_ltac.out
@@ -4,7 +4,7 @@ Ltac t2 := let x := string:("my tactic") in
x
Ltac t3 := idtacstr "my tactic"
Ltac t4 x := match x with
- | ?A => (A, A)
+ | ?A => constr:((A, A))
end
The command has indeed failed with message:
idnat is bound to a notation that does not denote a reference.
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index cdbcc24484..3ce50865c0 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1362,7 +1362,7 @@ let () =
let () =
let e = Tac2entries.Pltac.tac2expr_in_env in
- let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (in_gen (rawwit wit_ltac2) v) in
+ let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some "ltac2", in_gen (rawwit wit_ltac2) v) in
Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None)
(* Ltac1 runtime representation of Ltac2 closure quotations *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:54:13 +0000