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 $@

_CoqProject

 -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

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.

theories/stdpp_options.v

+Generalizable All Variables.
+Set Automatic Coercions Import.
+Set Asymmetric Patterns.
+Unset Transparent Obligations.
+Obligation Tactic := idtac.