A shortcut for coq-insert-as-in-next-command.

Works well for a single induction/destruct.
Works sometimes for inversion.
Does not work in presence of eqn flag yet (easy to fix).
Does not work on ;-combined tactics (hard to fix).
Does not work on a lot of inversion invocation (but some are ok).

We basically need another "as" tactical with a retro-predictable input.
That is: when seeing the resulting goal we can deduce what would have
been the right "as" close. This is currently the case only for
destruct/induction !foo (notice the exclamation mark).

1 files changed, 13 insertions, 8 deletions

diff --git a/coq/coq.el b/coq/coq.el
index d9a04bc5..9c55a195 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -2313,14 +2313,15 @@ Warning: this makes the error messages (and location) wrong.")
 ;; Trying to propose insertion of "as" for a whole region. But iterating
 ;; proof-assert-next-command-interactive is probably wrong if some error occur
 ;; during scripting.
-(defun coq-insert-as-in-region (&optional beg end)
-  (interactive "r")
-  (let ((beg (or beg (point-min)))
-        (end (or end (point-max))))
-    (goto-char beg)
-    (while (< (point) end)
-      (coq-script-parse-cmdend-forward)
-      (proof-assert-next-command-interactive))))
+;; (defun coq-insert-as-in-region (&optional beg end)
+;;   (interactive "r")
+;;   (let ((beg (or beg (point-min)))
+;;         (end (or end (point-max))))
+;;     (goto-char beg)
+;;     (while (< (point) end)
+;;       (coq-script-parse-cmdend-forward)
+;;       (coq-insert-as-in-next-command)
+;;       (proof-assert-next-command-interactive))))
 
 
 
@@ -2404,6 +2405,9 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-keymap [(control return)] 'coq-insert-command)
 (define-key coq-keymap [(control ?q)] 'coq-query)
 (define-key coq-keymap [(control ?r)] 'coq-insert-requires)
+; [ for "as [xxx]" is easy to remember, ccontrol-[ would be better but hard to type on french keyboards
+; anyway company-coq should provide an "as!<TAB>". 
+(define-key coq-keymap [(?\[)] 'coq-insert-as-in-next-command) ;; not for goal/response buffer?
 
 ; Query commands
 (define-key coq-keymap [(control ?s)] 'coq-Show)
@@ -2419,6 +2423,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-keymap [(control ?l)] 'coq-LocateConstant)
 (define-key coq-keymap [(control ?n)] 'coq-LocateNotation)
 (define-key coq-keymap [(control ?w)] 'coq-ask-adapt-printing-width-and-show)
+
 ;(proof-eval-when-ready-for-assistant
 ; (define-key ??? [(control c) (control a)] (proof-ass keymap)))