Span menu entry for proof using annotation + doc.

1 files changed, 10 insertions, 20 deletions

diff --git a/CHANGES b/CHANGES
index 013dc3be..9713ea0e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -47,26 +47,16 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac
 
 *** Automatic insertion of "Proof using" annotations.
 
-    When "Suggest Proof Using" is set in coq, coq suggests "Proof
-    using" annotations when it detects there is no such annotation (or
-    a wrong one) in you proof and there should be one (i.r. you are
-    inside a section). By default PG will ask the user before
-    inserting the suggested annotation. You can customize this
-    behaviour:
-
-    (setq coq-accept-proof-using-suggestion 'always)
-    or
-    (setq coq-accept-proof-using-suggestion 'never)
-    or (default)
-    (setq coq-accept-proof-using-suggestion 'ask)
-
-    This is also settable from Coq menu.
-
-    Limitations:
-    - do not support nested proofs.
-    - always use the first suggestion (coq can provide several solutions).
-    - the proof is not replayed, which is consistent with the fact
-      that pg do not deal with async proofs.
+    PG now supports the "Suggest Proof Using" by inserting
+    (automatically or by contextual menu or by a command) the "Proof
+    using" annotation suggested by Coq. This suggestion happens at
+    "Qed" command. By default PG will only highlight the corresponding
+    "Proof" keyword and let the user actively ask for insertion. You
+    can customize this behaviour by setting the
+    coq-accept-proof-using-suggestion to one of these values: 'always,
+    'highlight, 'ask, 'never. This is also settable from Coq menu. See
+    documentation of this variable for an explanation of the different
+    possible values and some more information.
 
 *** Limited extensibility for indentation