diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ff66d915f5..d6a334c5fe 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -293,7 +293,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err ~hdr:"Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" @@ -773,9 +773,7 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = String.copy (string_of_modfile mp) in - if s.[0] != s0.[0] then s.[0] <- s0.[0]; - s + String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp) let add_blacklist_entries l = blacklist_table := |