From 0c32a39131f62ff1b19f4395d28c057b64074eb6 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 9 Jul 2012 22:26:02 +0000 Subject: Added completion to insert Require, based on coq-load-path. --- CHANGES | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index 10e07512..d9b7dce8 100644 --- a/CHANGES +++ b/CHANGES @@ -21,14 +21,20 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. ** Coq changes +*** Multiple file handling for Coq Feature. + + No more experimental. Set coq-load-path to the list of directories + for libraries (you can attach it to the file using menu "coq prog + args"). + *** Support proof-tree visualization *** Indentation improvements using SMIE Still experimental. -** Limitations: +**** Limitations: -**** hard-wired precedence between bullets: - < + < * +***** hard-wired precedence between bullets: - < + < * example: Proof. - split. @@ -40,10 +46,9 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. - auto. Qed. -**** Always use "Proof." when proving an "Instance". - (wrong indentation and slow downs otherwise) - As a general rule, try to always introduce a proof with "Proof." - (or "Next Obligation"). +***** Always use "Proof." when proving an "Instance". (wrong + indentation and slow downs otherwise) As a general rule, try to + always introduce a proof with "Proof." (or "Next Obligation"). *** Minor parsing fixes @@ -51,6 +56,8 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** New commands for Print/Check/Show with Printing All flag +*** "Insert Requires" now uses completion based on coq-load-path + ** HOL Light [WORK IN PROGRESS] *** Basic support now works, see hol-light directory [WORK IN PROGRESS] -- cgit v1.2.3