| Index Entry | Section |
|---|
|
| . | | |
|---|
| .dir-locals.el | 10.2.1 Changing the name of the coq project file |
|
| _ | | |
|---|
| _CoqProject | 10.2 Using the Coq project file |
|
| A | | |
|---|
| active scripting buffer | 2.3.3 Active scripting buffer |
| Alt | 1.5 Prerequisites for this manual |
| annotation | 3.1 Document centred working |
| Assertion | 2.3.1 Locked, queue, and editing regions |
| Assertion | 3.7 Asserting across files |
| auto raise | 8.3 Display customization |
| Automatic processing | 3.2 Automatic processing |
| autosend | 3.2 Automatic processing |
|
| B | | |
|---|
| blue text | 2.3.1 Locked, queue, and editing regions |
| buffer display customization | 8.3 Display customization |
|
| C | | |
|---|
| Centaur | History of Proof General |
| colour | 5.1 Syntax highlighting |
| completion | 5.4 Support for completion |
| CtCoq | History of Proof General |
| Customization | 8. Customizing Proof General |
|
| D | | |
|---|
| Dedicated windows | 8.4 User options |
| display customization | 8.3 Display customization |
|
| E | | |
|---|
| EasyCrypt Proof General | 11. EasyCrypt Proof General |
| Editing region | 2.3.1 Locked, queue, and editing regions |
| Emacs customization library | 8.2 How to customize |
|
| F | | |
|---|
| Features | 1.3 Features of Proof General |
| file variables | 9.2 Using file variables |
| font lock | 5.1 Syntax highlighting |
| frames | 8.3 Display customization |
| Future | Future |
|
| G | | |
|---|
| generic | History of Proof General |
| goal | 2.3.2 Goal-save sequences |
| goal-save sequences | 2.3.2 Goal-save sequences |
| goals buffer | 2.4 Summary of Proof General buffers |
| Greek letters | 4. Unicode symbols and special layout support |
|
| H | | |
|---|
| history | History of Proof General |
|
| I | | |
|---|
| Imenu | 5.2 Imenu and Speedbar |
| Indentation | 8.4 User options |
| index menu | 5.2 Imenu and Speedbar |
| Input ring | 3.11 Editing features |
| Input ring | 8.4 User options |
|
| K | | |
|---|
| key sequences | 1.5 Prerequisites for this manual |
| keybindings | 9.1 Adding your own keybindings |
|
| L | | |
|---|
| Locked region | 2.3.1 Locked, queue, and editing regions |
| logical symbols | 4. Unicode symbols and special layout support |
|
| M | | |
|---|
| maintenance | Credits |
| mathematical symbols | 4. Unicode symbols and special layout support |
| Maths Menu | 4. Unicode symbols and special layout support |
| Meta | 1.5 Prerequisites for this manual |
| multiple file support | 10.4 Multiple File Support |
| Multiple Files | 3. Advanced Script Management and Editing |
| multiple frames | 8.3 Display customization |
| multiple windows | 8.3 Display customization |
|
| N | | |
|---|
| news | News for Version 4.6 |
| news | News for Version 4.5 |
| news | News for Version 4.4 |
| news | News for Version 4.3 |
| news | News for Version 4.2 |
| news | News for Version 4.1 |
| news | News for Version 4.0 |
| news | Old News for 3.1 |
| news | Old News for 3.2 |
|
| O | | |
|---|
| Omitting proofs for speed | 10.5 Omitting proofs for speed |
| opam-switch-mode support | 10.13 Opam-switch-mode support |
| outline mode | 5.3 Support for outline mode |
|
| P | | |
|---|
| pink text | 2.3.1 Locked, queue, and editing regions |
| prefix argument | 2.6 Script processing commands |
| proof assistant | 1. Introducing Proof General |
| proof by pointing | 2.4 Summary of Proof General buffers |
| proof by pointing | History of Proof General |
| Proof General | 1. Introducing Proof General |
| Proof General Kit | Future |
| proof script | 2.2 Proof scripts |
| Proof script indentation | 8.4 User options |
| proof script mode | 2.3 Script buffers |
| Proof status statistic | 3.8 Proof status statistic |
| Proof using | 10.3 Proof using annotations |
| proof-tree visualization | 7. Graphical Proof-Tree Visualization |
| Proof-Tree visualization | 10.11 Proof-Tree Visualization |
|
| Q | | |
|---|
| Query program name | 8.4 User options |
| Queue region | 2.3.1 Locked, queue, and editing regions |
|
| R | | |
|---|
| Remote host | 8.4 User options |
| Remote shell | 8.4 User options |
| response buffer | 2.4 Summary of Proof General buffers |
| Retraction | 2.3.1 Locked, queue, and editing regions |
| Retraction | 3.6 Retracting across files |
| Running proof assistant remotely | 8.4 User options |
|
| S | | |
|---|
| save | 2.3.2 Goal-save sequences |
| script buffer | 2.3 Script buffers |
| script management | History of Proof General |
| scripting | 2.2 Proof scripts |
| Shell | 3.10 Escaping script management |
| shell buffer | 2.4 Summary of Proof General buffers |
| Shell Proof General | 12. Shell Proof General |
| Showing Proof Diffs | 10.12 Showing Proof Diffs |
| Speedbar | 5.2 Imenu and Speedbar |
| Strict read-only | 8.4 User options |
| structure editor | History of Proof General |
| subscripts | 4. Unicode symbols and special layout support |
| superscripts | 4. Unicode symbols and special layout support |
| Switching between proof scripts | 3.4 Switching between proof scripts |
| symbols | 4. Unicode symbols and special layout support |
|
| T | | |
|---|
| tags | 5.5 Support for tags |
| three-buffer interaction | 8.3 Display customization |
| Tokens Mode | 4. Unicode symbols and special layout support |
| Toolbar button enablers | 8.4 User options |
| Toolbar disabling | 8.4 User options |
| Toolbar follow mode | 8.4 User options |
|