From 8b9c985c4efdb4579338bbae28a651974e31419c Mon Sep 17 00:00:00 2001
From: cyrilzak31
Date: Thu, 9 Apr 2020 15:55:46 +0200
Subject: Close #479

---
 coq/coq.el | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'coq')

diff --git a/coq/coq.el b/coq/coq.el
index 0c934a9b..dfed356c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2502,17 +2502,21 @@ mouse activation."
           (progn (end-of-line) (point)))))))
       (insert (concat "End" section)))))
 
+
 (defun coq--format-intros (output)
-  "Create an “intros” form from the OUTPUT of “Show Intros”."
+  "Create an “intros” or ”move” form from the OUTPUT of “Show Intros”."
   (let* ((shints1 (replace-regexp-in-string "^[0-9] subgoal\\(.\\|\n\\|\r\\)*"  "" output))
          (shints (replace-regexp-in-string "[\r\n ]*\\'" "" shints1)))
     (if (or (string= "" shints)
             (string-match coq-error-regexp shints))
         (error "Don't know what to intro")
-      (format "intros %s" shints))))
+      (save-excursion
+        (if (re-search-backward "Require.*ssreflect" nil t)
+            (format "move=> %s" shints)
+          (format "intros %s" shints))))))
 
 (defun coq-insert-intros ()
-  "Insert an intros command with names given by Show Intros.
+  "Insert an intros or move command with names given by Show Intros.
 Based on idea mentioned in Coq reference manual."
   (interactive)
   (let* ((output (proof-shell-invisible-cmd-get-result "Show Intros.")))
-- 
cgit v1.2.3