From d730a3371497723851d632966ac464d96fdc3c59 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Feb 2017 13:08:58 +0100
Subject: [PATCH] Options file.

---
 Makefile                 | 3 ---
 _CoqProject              | 3 +++
 theories/base.v          | 5 -----
 theories/stdpp_options.v | 5 +++++
 4 files changed, 8 insertions(+), 8 deletions(-)
 create mode 100644 theories/stdpp_options.v

diff --git a/Makefile b/Makefile
index 87749227..8de6ba81 100644
--- a/Makefile
+++ b/Makefile
@@ -3,9 +3,6 @@ ifeq ($(Y), 1)
 	YFLAG=-y
 endif
 
-# Configure Coq warnings
-COQ_MAKEFILE_FLAGS ?= -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-
 # Forward most targets to Coq makefile (with some trick to make this phony)
 %: Makefile.coq phony
 	+@make -f Makefile.coq $@
diff --git a/_CoqProject b/_CoqProject
index a7869b13..77dae218 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,4 +1,7 @@
 -Q theories stdpp
+-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
+-arg -l -arg stdpp_options
+theories/stdpp_options.v
 theories/option.v
 theories/fin_map_dom.v
 theories/bset.v
diff --git a/theories/base.v b/theories/base.v
index 65233ddf..6c2b35be 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -4,15 +4,10 @@
 that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, collections, and various other data
 structures. *)
-Global Generalizable All Variables.
-Global Set Automatic Coercions Import.
-Global Set Asymmetric Patterns.
-Global Unset Transparent Obligations.
 From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
 Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
-Obligation Tactic := idtac.
 
 (** Sealing off definitions *)
 Set Primitive Projections.
diff --git a/theories/stdpp_options.v b/theories/stdpp_options.v
new file mode 100644
index 00000000..b2b00867
--- /dev/null
+++ b/theories/stdpp_options.v
@@ -0,0 +1,5 @@
+Generalizable All Variables.
+Set Automatic Coercions Import.
+Set Asymmetric Patterns.
+Unset Transparent Obligations.
+Obligation Tactic := idtac.
-- 
GitLab