diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 74728f412..51946871f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -242,7 +242,7 @@ let safe_basename_of_global r = let last_chance r = try Nametab.basename_of_global r with Not_found -> - anomaly "Inductive object unknown to extraction and not globally visible" + anomaly (Pp.str "Inductive object unknown to extraction and not globally visible") in match r with | ConstRef kn -> Label.to_id (con_label kn) |