diff options
| author | Pierre Courtieu | 2020-04-09 16:01:50 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2020-04-09 16:01:50 +0200 |
| commit | 4dba3f78e50604d899ef80bfda45c5aa4467adeb (patch) | |
| tree | 6f9616bf1d131df2df30b3add49039fe11bcd25c | |
| parent | 420dc6a4b9bc61b3c13c5e7c3dce2521c120baaa (diff) | |
Unplugging previous commit (proof using insertion.
It needs more tweaking when a bloc is asserted at once.
| -rw-r--r-- | coq/coq.el | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -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... ;;;;;;;;;; |
