diff options
| author | kristerw <kristerw> | 2003-03-22 20:21:16 +0000 |
|---|---|---|
| committer | kristerw <kristerw> | 2003-03-22 20:21:16 +0000 |
| commit | 7f7fda3da76470a33ff44b47dd85771f08b91c71 (patch) | |
| tree | 7eb193bdfae6b63163d62dd8c922ea2115b80fda /lang/coq/MESSAGE | |
| parent | c30905eb2550b833127b5e70f5f7c49aa84703fc (diff) | |
| download | pkgsrc-7f7fda3da76470a33ff44b47dd85771f08b91c71.tar.gz | |
By popular demand, move coq-7.4 from math to lang in order to be consistent
with prior art (e.g. lang/twelf).
Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.
Diffstat (limited to 'lang/coq/MESSAGE')
| -rw-r--r-- | lang/coq/MESSAGE | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/lang/coq/MESSAGE b/lang/coq/MESSAGE new file mode 100644 index 00000000000..d45993a5d2e --- /dev/null +++ b/lang/coq/MESSAGE @@ -0,0 +1,14 @@ +=========================================================================== +$NetBSD: MESSAGE,v 1.1.1.1 2003/03/22 20:21:16 kristerw Exp $ + +You may wish to add the following to your ~/.emacs: + + (add-to-list 'auto-mode-alist '("\\.v$" . coq-mode)) + (autoload 'coq-mode "coq" "Major mode for editing Coq vernacular." t) + (autoload 'run-coq "coq-inferior" "Run an inferior Coq process." t) + (autoload 'run-coq-other-window "coq-inferior" + "Run an inferior Coq process in a new window." t) + (autoload 'run-coq-other-frame "coq-inferior" + "Run an inferior Coq process in a new frame." t) + +=========================================================================== |