From 5360fb1202375d90adde5c8ba6700098e57bed53 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Feb 2020 14:12:51 +0100
Subject: Fix #11552: Ltac2 breaks query commands during proofs.

Actually, callers of the Pvernac.register_proof_mode function have to
manually register the parsing of vernacular queries themselves. This
probably qualifies as an oversight from myself.
---
 user-contrib/Ltac2/g_ltac2.mlg | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index c1bd585f3f..d05640f22d 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -948,6 +948,12 @@ VERNAC { tac2mode } EXTEND VernacLtac2
   fun ~pstate -> Tac2entries.call ~pstate ~default t }
 END
 
+GRAMMAR EXTEND Gram
+  GLOBAL: tac2mode;
+  tac2mode:
+    [ [ tac = G_vernac.query_command -> { tac None } ] ];
+END
+
 {
 
 open Stdarg
-- 
cgit v1.2.3