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/tacsubst.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

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