Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.

11 files changed, 28 insertions, 27 deletions

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) ] -> {