aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/configure.ml b/configure.ml
index 194f47c49..0b6b47e9a 100644
--- a/configure.ml
+++ b/configure.ml
@@ -647,8 +647,9 @@ let camltag = match caml_version_list with
48: implicit elimination of optional arguments: too common
50: unexpected documentation comment: too common and annoying to avoid
56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
+ 59: "potential assignment to a non-mutable value": See Coq's issue #8043
*)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-59"
let coq_warn_error =
if !prefs.warn_error
then "-warn-error +a"