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.
---
 test-suite/bugs/closed/bug_11552.v | 9 +++++++++
 user-contrib/Ltac2/g_ltac2.mlg     | 6 ++++++
 2 files changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11552.v

diff --git a/test-suite/bugs/closed/bug_11552.v b/test-suite/bugs/closed/bug_11552.v
new file mode 100644
index 0000000000..189b1d9d8a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11552.v
@@ -0,0 +1,9 @@
+From Ltac2 Require Import Ltac2.
+
+Goal True.
+Proof.
+  Search unit.
+  (* Unbound constructor Search *)
+  Check tt.
+  (* Unbound constructor Check *)
+Abort.
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