diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 19 |
1 files changed, 18 insertions, 1 deletions
@@ -49,7 +49,23 @@ RECDIRS += MenhirLib COQINCLUDES += -R MenhirLib MenhirLib endif -COQCOPTS ?= -w -undeclared-scope -w -omega-is-deprecated +# Notes on silenced Coq warnings: +# +# undeclared-scope: +# warning introduced in 8.12 +# suggested change (use `Declare Scope`) supported since 8.12 +# unused-pattern-matching-variable: +# warning introduced in 8.13 +# the code rewrite that avoids the warning is not desirable +# deprecated-ident-entry: +# warning introduced in 8.13 +# suggested change (use `name` instead of `ident`) supported since 8.13 + +COQCOPTS ?= \ + -w -undeclared-scope \ + -w -unused-pattern-matching-variable \ + -w -deprecated-ident-entry + COQC="$(COQBIN)coqc" -q $(COQINCLUDES) $(COQCOPTS) COQDEP="$(COQBIN)coqdep" $(COQINCLUDES) COQDOC="$(COQBIN)coqdoc" @@ -65,6 +81,7 @@ GPATH=$(DIRS) ifeq ($(LIBRARY_FLOCQ),local) FLOCQ=\ + SpecFloatCompat.v \ Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v \ Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v \ Bracket.v Div.v Operations.v Round.v Sqrt.v \ |