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 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'CHANGES') 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 -- cgit v1.2.3