Commit d730a337 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Options file.

parent 2c261344
...@@ -3,9 +3,6 @@ ifeq ($(Y), 1) ...@@ -3,9 +3,6 @@ ifeq ($(Y), 1)
YFLAG=-y YFLAG=-y
endif 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) # Forward most targets to Coq makefile (with some trick to make this phony)
%: Makefile.coq phony %: Makefile.coq phony
+@make -f Makefile.coq $@ +@make -f Makefile.coq $@
......
-Q theories stdpp -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/option.v
theories/fin_map_dom.v theories/fin_map_dom.v
theories/bset.v theories/bset.v
......
...@@ -4,15 +4,10 @@ ...@@ -4,15 +4,10 @@
that are used throughout the whole development. Most importantly it contains that are used throughout the whole development. Most importantly it contains
abstract interfaces for ordered structures, collections, and various other data abstract interfaces for ordered structures, collections, and various other data
structures. *) 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. From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Export ListNotations. Export ListNotations.
From Coq.Program Require Export Basics Syntax. From Coq.Program Require Export Basics Syntax.
Obligation Tactic := idtac.
(** Sealing off definitions *) (** Sealing off definitions *)
Set Primitive Projections. Set Primitive Projections.
......
Generalizable All Variables.
Set Automatic Coercions Import.
Set Asymmetric Patterns.
Unset Transparent Obligations.
Obligation Tactic := idtac.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment