Fixed #1 (Missing space in coq-insert-intros).

Added a newline and removed the useless intros.

1 files changed, 5 insertions, 3 deletions

diff --git a/coq/coq.el b/coq/coq.el
index ea2da5d0..8cf818dd 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2065,12 +2065,14 @@ mouse activation."
 Based on idea mentioned in Coq reference manual."
   (interactive)
   (let* ((shints (proof-shell-invisible-cmd-get-result "Show Intros."))
-         (intros (replace-regexp-in-string "^\\([^\n]+\\)\n"  "intros \\1." shints t)))
+         ;; insert a dot before the trailing \n and put intros at begining
+         (intros (concat "intros " (substring shints 0 (- (length shints) 1)) ".\n")))
     (if (or (< (length shints) 2);; empty response is just NL
             (string-match coq-error-regexp shints))
         (error "Don't know what to intro")
-      (insert intros)
-      (indent-according-to-mode))))
+      (let ((pt (point)))
+        (insert intros)
+        (indent-region pt (point))))))
 
 
 (defvar coq-commands-accepting-as (regexp-opt '("induction" "destruct" "inversion" "injection")))