From 03cccc325821b6fff42d2e0a91dd9ce8ec7c3fea Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Tue, 5 Sep 2017 17:19:07 -0400
Subject: read flags from project file for Compile Buffer

---
 CHANGES       | 5 +++++
 ide/coqide.ml | 2 ++
 2 files changed, 7 insertions(+)

diff --git a/CHANGES b/CHANGES
index 4e40122d43..796fbd043d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -13,6 +13,11 @@ Tactics
   profiling, and "Set NativeCompute Profile Filename" customizes
   the profile filename.
 
+Tools
+
+- In CoqIDE, the "Compile Buffer" command takes account of flags in
+  _CoqProject or other project file.
+
 Changes from 8.6.1 to 8.7+beta
 ==============================
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 7b65c9fec9..6b24740b30 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -439,7 +439,9 @@ let compile sn =
   match sn.fileops#filename with
     |None -> flash_info "Active buffer has no name"
     |Some f ->
+      let (_,args) = make_coqtop_args fn in
       let cmd = cmd_coqc#get ^ " -I " ^ (Filename.quote (Filename.dirname f))
+	^ (List.fold_left (fun accum arg -> accum ^ " " ^ arg) "" args)
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-- 
cgit v1.2.3


From 8d5165155dc4d9e4c03507609bf1b7a24a8ce4d0 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 6 Sep 2017 12:13:42 -0400
Subject: use get_arguments, String.concat, remove -I

---
 ide/coqide.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 6b24740b30..2c8ce0049e 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -439,9 +439,9 @@ let compile sn =
   match sn.fileops#filename with
     |None -> flash_info "Active buffer has no name"
     |Some f ->
-      let (_,args) = make_coqtop_args fn in
-      let cmd = cmd_coqc#get ^ " -I " ^ (Filename.quote (Filename.dirname f))
-	^ (List.fold_left (fun accum arg -> accum ^ " " ^ arg) "" args)
+      let args = Coq.get_arguments sn.coqtop in
+      let cmd = cmd_coqc#get 
+	^ " " ^ String.concat " " args
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
-- 
cgit v1.2.3