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/tacintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

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