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 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11552.v

(limited to 'test-suite')

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