diff options
| author | Matthieu Sozeau | 2015-09-14 18:35:48 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-09-14 18:41:09 +0200 |
| commit | 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b (patch) | |
| tree | ce5b0fed1af0fb238a23d6b78a57a9bf2df29bb7 /Makefile.build | |
| parent | 490160d25d3caac1d2ea5beebbbebc959b1b3832 (diff) | |
Univs: Add universe binding lists to definitions
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index 6ceff2de95..0057b71684 100644 --- a/Makefile.build +++ b/Makefile.build @@ -94,6 +94,7 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +CAMLFLAGS:= $(CAMLFLAGS) -w +a-3-4-6-7-9-27-29-32..39-41..42-44-45-48 OCAMLC := $(OCAMLC) $(CAMLFLAGS) OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS) |