diff options
| author | Erik Martin-Dorel | 2020-04-02 20:01:28 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-02 20:01:28 +0200 |
| commit | 0204fb90c5b6bed081ab407c8d92e015cad99fdf (patch) | |
| tree | cc055dd0397f55e845308485c3c2586b4b59a9a7 /doc | |
| parent | 71748af5bc0f813d4c6a42f303d2c2cec85b3c9a (diff) | |
| parent | a03dc31801972cbcff38035a30711da34d66ed78 (diff) | |
Merge pull request #476 from dunnl/issue-475
Fix documentation about Coq electric terminator
Related: #160
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 699b304b..5f1e8231 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -924,8 +924,7 @@ example in Isabelle with semi-colons, but these will not appear in the final text. Coq, on the other hand, requires a full-stop terminator at the end of -each line, so @kbd{C-c .} is the key binding used to turn on -electric terminator. If you don't know what the terminator character +each line. If you don't know what the terminator character is, you can find the option anyway on the menu: @code{Proof-General -> Quick Options -> Processing -> Electric Terminator} which also shows the key binding. |