...
 
Commits (1)
......@@ -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 $@
......
-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
......
......@@ -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.
......
Generalizable All Variables.
Set Automatic Coercions Import.
Set Asymmetric Patterns.
Unset Transparent Obligations.
Obligation Tactic := idtac.