Is it possible to automatically complete the externally defined symbols and tactics in Coq 8.7.

[ginqi7]

Hello, I just started using company-coq.

I read README and learned that if I wanted to automatically complete the externally defined symbols and tactics I needed a patch in the old Coq version.

Now i'm using Coq 8.7, what do i need to do?

Thank you.

[cpitclaudel]

Sorry for the delay. I think simply adding (setq company-coq-live-on-the-edge t) to your init file should be enough :)

[ginqi7]

Thank you for your reply.

I added this configuration to my init file, it still does not work.

The variable has been set successfully.

My requirement is that when I define a theorem_A in file_1 and then import file_1 into file_2, I want to automatically fill in its name when I apply theorem_A.

My configuration about company-coq is:

  (load "~/.emacs.d/lisp/PG/generic/proof-site")
  (add-hook 'coq-mode-hook #'company-coq-mode)
  (setq company-coq-live-on-the-edge t)

My configuration about company is :

  (use-package company
    :defer t
    :diminish ""
    :bind ("C-." . company-complete)
    :init
    (add-hook 'prog-mode-hook 'company-mode)
    :config
    (progn
      (setq company-idle-delay 0.1
            company-minimum-prefix-length 0
            company-selection-wrap-around t
            company-show-numbers t
            company-dabbrev-downcase nil
            company-transformers '(company-sort-by-occurrence))
      (bind-keys :map company-active-map
                 ("C-n" . company-select-next)
                 ("C-p" . company-select-previous)
                 ("C-d" . company-show-doc-buffer)
                 ("<tab>" . company-complete))))

My Emacs version is 25.3.1, Coq version is 8.7.0, company-coq is installed from MELPA.

My description is verbose, thanks for your patience.