From 4dba3f78e50604d899ef80bfda45c5aa4467adeb Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 9 Apr 2020 16:01:50 +0200
Subject: Unplugging previous commit (proof using insertion.

It needs more tweaking when a bloc is asserted at once.
---
 coq/coq.el | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index 610f1c42..48be8f37 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2614,8 +2614,8 @@ recieving suggestions from coq at Qed time."
         (coq-insert-proof-using-suggestion suggestion)))))
 
 
-(add-hook 'proof-shell-handle-delayed-output-hook
-	  #'coq-proof-using-suggest-hook t)
+;(add-hook 'proof-shell-handle-delayed-output-hook
+	  ;#'coq-proof-using-suggest-hook t)
 
 
 ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;;
-- 
cgit v1.2.3