From 8dc8561b71646db2342d6aac86d654a386478219 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 4 Jul 2013 12:22:34 +0000
Subject: Fixing undeclared variables for compilation.

---
 CHANGES    | 7 ++++++-
 coq/coq.el | 2 ++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 10d7c4c2..7a1d34b1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -30,7 +30,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
 
 *** Support for bullets, braces and Grab Existential Variables for Prooftree.
 
-*** Suuport for _Coqproject files
+*** Support for _Coqproject files
 
     According to Coq documentation, it is advised to use coq_makefile
     -f _CoqProject -o Makefile to build your Makefile automatically
@@ -46,6 +46,11 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac.
     the use of local file variables (which remains possible and
     overrides project file options).
 
+*** Automatic insertion of "as" clauses.
+
+    Should work for induction and destruct for now. Toggle this option
+    with Coq/Settings/Auto insert As.
+
 * Changes of Proof General 4.2 from Proof General 4.1
 
 ** Generic/misc changes
diff --git a/coq/coq.el b/coq/coq.el
index e0fb309c..336f6205 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -26,6 +26,8 @@
   (defvar string nil)       ; dynamic scope in coq-insert-as stuff
   (defvar coq-auto-insert-as nil)    ; defpacustom
   (defvar coq-time-commands nil)        ; defpacustom
+  (defvar use-project-file t)        ; defpacustom
+  (defvar coq-project-filename nil)        ; defpacustom
   (defvar coq-use-editing-holes nil)    ; defpacustom
   (defvar coq-hide-additional-subgoals nil) ; defpacustom
   (proof-ready-for-assistant 'coq))     ; compile for coq
-- 
cgit v1.2.3