diff options
Diffstat (limited to 'doc/sphinx/practical-tools/utilities.rst')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 63 |
1 files changed, 1 insertions, 62 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5dba92429..bdaa2aa1a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -950,71 +950,10 @@ There are options to produce the |Coq| parts in smaller font, italic, between horizontal rules, etc. See the man page of ``coq-tex`` for more details. -|Coq| and GNU Emacs ------------------------ - - -The |Coq| Emacs mode -~~~~~~~~~~~~~~~~~~~~~~~~~ - -|Coq| comes with a Major mode for GNU Emacs, ``gallina.el``. This mode -provides syntax highlighting and also a rudimentary indentation -facility in the style of the ``Caml`` GNU Emacs mode. - -Add the following lines to your ``.emacs`` file: - -:: - - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) - - -The |Coq| major mode is triggered by visiting a file with extension ``.v``, -or manually with the command ``M-x coq-mode``. It gives you the correct -syntax table for the |Coq| language, and also a rudimentary indentation -facility: - - -+ pressing ``Tab`` at the beginning of a line indents the line like the - line above; -+ extra tabulations increase the indentation level (by 2 spaces by default); -+ ``M-Tab`` decreases the indentation level. - - -An inferior mode to run |Coq| under Emacs, by Marco Maggesi, is also -included in the distribution, in file ``inferior-coq.el``. Instructions to -use it are contained in this file. - - -Proof-General -~~~~~~~~~~~~~ - -Proof-General is a generic interface for proof assistants based on -Emacs. The main idea is that the |Coq| commands you are editing are sent -to a |Coq| toplevel running behind Emacs and the answers of the system -automatically inserted into other Emacs buffers. Thus you don’t need -to copy-paste the |Coq| material from your files to the |Coq| toplevel or -conversely from the |Coq| toplevel to some files. - -Proof-General is developed and distributed independently of the system -|Coq|. It is freely available at `<https://proofgeneral.github.io/>`_. - - -Module specification --------------------- - -Given a |Coq| vernacular file, the gallina filter extracts its -specification (inductive types declarations, definitions, type of -lemmas and theorems), removing the proofs parts of the file. The |Coq| -file ``file.v`` gives birth to the specification file ``file.g`` (where -the suffix ``.g`` stands for |Gallina|). - -See the man page of ``gallina`` for more details and options. - Man pages --------- -There are man pages for the commands ``coqdep``, ``gallina`` and ``coq-tex``. Man +There are man pages for the commands ``coqdep`` and ``coq-tex``. Man pages are installed at installation time (see installation instructions in file ``INSTALL``, step 6). |