From 3994c276922f94f34943db938423c40a05b4d9da Mon Sep 17 00:00:00 2001
From: Patrick Loiseleur
Date: Mon, 14 Jun 1999 15:26:46 +0000
Subject: Added coq-begin-Section and coq-end-Section

---
 doc/ProofGeneral.texi | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 76640043..44692af8 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1,3 +1,4 @@
+
 \input texinfo   @c -*-texinfo-*-
 @c
 @c $Id$
@@ -1929,6 +1930,8 @@ General.
 @kindex C-c C-s
 @kindex C-c I 
 @kindex C-c a
+@kindex C-c s
+@Kindex C-c e
 
 Coq Proof General supplies the following key-bindings:
 @table @kbd
@@ -1939,6 +1942,11 @@ Inserts ``Apply '' into proof buffer.
 @item C-c C-s
 Runs Coq's search utility on a user-provided string, using
 the @code{Search} command of Coq.
+@item C-c s
+Inserts ``Section '' into proof buffer
+@item C-c e
+Closes the current section by inserting ``End <section-name>.''. (this
+should work well with nested sections).
 @end table
 
 @node Editing multiple proofs
-- 
cgit v1.2.3