From d286c3601e24afe0a681d092cbd880773872b980 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 15 Sep 2020 21:24:39 +0200
Subject: Fixes #9716, #13004: don't drop the qualifier of quotations at
 printing time.

---
 plugins/ltac/tacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ltac/tacexpr.ml')

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
-- 
cgit v1.2.3