emacsproof-general

How to disable Verilog mode in emacs?


I'm trying to use coq with ProofGeneral, but the built-in Verilog mode shadows *.v filetype recognition. Can I somehow disable it and let ProofGeneral remap them to its coq mode?


Solution

  • You are going to have to override the binding in auto-mode-alist in your .emacs or whatnot.

    This SO post does something similar with VHDL:

    How do I turn off vhdl-mode in emacs?

    Also, I googled for "auto-mode-alist remove" and found this link. Copy/Pasting the important bit:

    ;; Remove all annoying modes from auto mode lists
    
    (defun replace-alist-mode (alist oldmode newmode)
      (dolist (aitem alist)
        (if (eq (cdr aitem) oldmode)
        (setcdr aitem newmode))))
    
    ;; not sure what mode you want here. You could default to 'fundamental-mode
    (replace-alist-mode auto-mode-alist 'verilog-mode 'proof-general-mode)