From f9db893de2569bba596dd74b2e51ae0e0406dbe7 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 21 Jun 2013 14:39:52 +0000 Subject: Added an entry to CHANGEs about coq project fields. --- CHANGES | 15 +++++++++++++++ 1 file changed, 15 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index e2969690..10d7c4c2 100644 --- a/CHANGES +++ b/CHANGES @@ -30,6 +30,21 @@ 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 + + According to Coq documentation, it is advised to use coq_makefile + -f _CoqProject -o Makefile to build your Makefile automatically + from "profect file" _CoqProject. Such a file should contains the + options to pass to coq_makefile, i.e. paths to add to coq load + path (-I, -R) and other options to pass to coqc/coqtop (-arg). + + Coqide (and now proofgeneral) do use the information stored in + this file to configure the options to add to the coqtop + invocation. When opening a coq file, proofgeneral looks for a file + _Coqproject in the current directory or a parent directory and + reads it. Except for very unlikely situation this should replace + the use of local file variables (which remains possible and + overrides project file options). * Changes of Proof General 4.2 from Proof General 4.1 -- cgit v1.2.3