diff options
Diffstat (limited to 'plugins/xml')
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 6145548b2..d065ba61a 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -380,10 +380,7 @@ let print internal glob_ref kind xml_library_root = match glob_ref with Gn.VarRef id -> (* this kn is fake since it is not provided by Coq *) - let kn = - let (mod_path,dir_path) = Lib.current_prefix () in - N.make_kn mod_path dir_path (N.Label.of_id id) - in + let kn = Lib.make_kn id in let (_,body,typ) = G.lookup_named id in Cic2acic.Variable kn,mk_variable_obj id body typ | Gn.ConstRef kn -> |