diff options
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/cic2acic.ml | 4 | ||||
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 5bb7635b9d..7706a3eb59 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -80,7 +80,7 @@ let get_uri_of_var v pvars = type tag = Constant of Names.constant - | Inductive of Names.kernel_name + | Inductive of Names.mutual_inductive | Variable of Names.kernel_name ;; @@ -165,7 +165,7 @@ let token_list_of_kernel_name tag = N.id_of_label (N.con_label con), Lib.remove_section_part (LN.ConstRef con) | Inductive kn -> - N.id_of_label (N.label kn), + N.id_of_label (N.mind_label kn), Lib.remove_section_part (LN.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index a46500b89c..294f5154d3 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) ;; |