From 4322481d0509a9817935bf22ceb2a5be43a81892 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 26 Dec 2016 17:36:53 +0100 Subject: Fix doc for Coq electric terminator. Close ProofGeneral/PG#138. --- doc/ProofGeneral.texi | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/ProofGeneral.texi') diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 40c0ef87..442ce6d5 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -920,7 +920,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 C-.} is the key binding used to turn on +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 is, you can find the option anyway on the menu: @code{Proof-General -> Quick Options -> Processing -> Electric Terminator} -- cgit v1.2.3