Added completion to insert Require, based on coq-load-path.

1 files changed, 13 insertions, 6 deletions

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]