diff options
Diffstat (limited to 'utils/warnings.mli')
| -rw-r--r-- | utils/warnings.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/utils/warnings.mli b/utils/warnings.mli index cb55f8c60..1610b3c3a 100644 --- a/utils/warnings.mli +++ b/utils/warnings.mli @@ -38,6 +38,7 @@ type t = (* A is all *) | Camlp4 of string | All_clauses_guarded | Useless_record_with + | Bad_module_name of string | Unused_var of string (* Y *) | Unused_var_strict of string (* Z *) ;; |