Skip to content

Commit

Permalink
Flocq no longer triggers the opaque-let warning
Browse files Browse the repository at this point in the history
This has been addressed upstream, apparently.
  • Loading branch information
xavierleroy committed Nov 27, 2024
1 parent c9df468 commit ba046c3
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -57,15 +57,11 @@ endif
# deprecated-instance-without-locality:
# warning introduced in 8.14
# triggered by Menhir-generated files, to be solved upstream in Menhir
# opaque-let:
# warning introduced in 8.18, addressed in the main CompCert files,
# still triggered by Flocq, to be solved upstream

COQCOPTS ?= \
-w -unused-pattern-matching-variable

cparser/Parser.vo: COQCOPTS += -w -deprecated-instance-without-locality
flocq/IEEE754/Bits.vo: COQCOPTS += -w -opaque-let
MenhirLib/Interpreter.vo: COQCOPTS += -w -undeclared-scope

ifneq ($(INSTALL_COQDEV),true)
Expand Down

0 comments on commit ba046c3

Please sign in to comment.