From dcbcc4d1e765ea50d50fdb9d75378e4166472b71 Mon Sep 17 00:00:00 2001
From: Elijah Malaby <qwe12345678910@gmail.com>
Date: Sun, 2 Dec 2018 13:22:42 -0500
Subject: [PATCH] Added a popup rule to ignore proof general popups

---
 modules/lang/coq/config.el | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/modules/lang/coq/config.el b/modules/lang/coq/config.el
index eebd75636..7487ee9f2 100644
--- a/modules/lang/coq/config.el
+++ b/modules/lang/coq/config.el
@@ -6,6 +6,8 @@
 (setq coq-mode-abbrev-table '())
 
 (after! company-coq
+  (set-popup-rules!
+    '(("^\\*\\(response\\|goals\\)\\*" :ignore t)))
   (set-lookup-handlers! 'company-coq-mode
     :definition #'company-coq-jump-to-definition
     :references #'company-coq-grep-symbol