diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index e0a6e843..497ddf03 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -255,7 +255,7 @@ let safe_basename_of_global r = let string_of_global r = try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r) - with _ -> string_of_id (safe_basename_of_global r) + with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r) let safe_pr_global r = str (string_of_global r) @@ -263,7 +263,7 @@ let safe_pr_global r = str (string_of_global r) let safe_pr_long_global r = try Printer.pr_global r - with _ -> match r with + with e when Errors.noncritical e -> match r with | ConstRef kn -> let mp,_,l = repr_con kn in str ((string_of_mp mp)^"."^(string_of_label l)) @@ -452,7 +452,7 @@ let my_bool_option name initval = (*s Extraction AccessOpaque *) -let access_opaque = my_bool_option "AccessOpaque" false +let access_opaque = my_bool_option "AccessOpaque" true (*s Extraction AutoInline *) |