diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index ab113928a..a3c1af98d 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -657,7 +657,7 @@ let print_mutual_inductive packs fv hyps env inner_types = let string_list_of_named_context_list = List.map - (function (n,_,_) -> Names.string_of_id n) + (function (n,_,_) -> Names.string_of_id (Names.basename n)) ;; let types_filename_of_filename = |