From 97b8d4fcdcd67d49acd59389795fc48d9fa8f1d0 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 10 Apr 2020 22:48:55 +0200 Subject: Span menu entry for proof using annotation + doc. --- CHANGES | 30 ++++++++++-------------------- 1 file changed, 10 insertions(+), 20 deletions(-) (limited to 'CHANGES') 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 -- cgit v1.2.3