diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index c58672ca0..502d06235 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -362,10 +362,6 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let error_record r = - err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++ - fnl () ++ str "To help extraction, please use an explicit name.") - let msg_non_implicit r n id = let name = match id with | Anonymous -> "" |