Coq prooftree: recognize "2 : {" as navigation command

Failing to recognize a parenthesis with a goal selector as a
navigation command first displays a wrong proof tree and eventually
triggers an assertion in prooftree when continuing after the
corresponding closing brace.

Author: hendriktews

coq/coq.el

@@ -242,7 +242,9 @@ It is mostly useful in three window mode, see also
 (defcustom coq-navigation-command-regexp
   (concat "^\\(\\(Focus\\)\\|\\(Unfocus\\)\\|"
           "\\(all\\s-*:\\s-*\\(cycle\\|swap\\|revgoals\\)\\)\\|"
-          "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|\\({\\)\\|\\(}\\)\\)")
+          "\\(\\+\\)\\|\\(-\\)\\|\\(\\*\\)\\|"
+          "\\(\\([0-9]+\\s-*:\\s-*\\)?{\\)\\|"
+          "\\(}\\)\\)")
   "Regexp for `proof-tree-navigation-command-regexp'."
   :type 'regexp
   :group 'coq-proof-tree)