---
name: "proofgeneral"
section: "1"
platform: "linux"
package: "proofgeneral"
version: "4.5-3"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/proofgeneral"
---

# proofgeneral(1)

start Emacs with the Proof General splash screen

## NAME

proofgeneral - start Emacs with the Proof General splash screen

## SYNOPSIS

**proofgeneral** files*...*

## DESCRIPTION

The command **proofgeneral** is just an abbreviation for  *emacs -f proof-splash-display-screen.* Thus it starts emacs, displays the Proof General splash screen and behaves otherwise identical to emacs.

Use **proofgeneral** *file.v* to start Proof General in Coq mode for  *file.v.*

## SEE ALSO

[**emacs**(1)](/emacs/1.md),

## AUTHOR

The  **proofgeneral** script and this manual page were written by Hendrik Tews \<hendrik@askra.de\>, specifically for the Debian project (and may be used by others).