diff options
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index a46500b89..294f5154d 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -629,7 +629,7 @@ let _ = let _ = Declare.set_xml_declare_inductive (function (isrecord,(sp,kn)) -> - print false (Libnames.IndRef (kn,0)) (kind_of_inductive isrecord kn) + print false (Libnames.IndRef (Names.mind_of_kn kn,0)) (kind_of_inductive isrecord (Names.mind_of_kn kn)) xml_library_root) ;; |