diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
| commit | f6d8fc17dc9474e4d043cf709d672d9259599354 (patch) | |
| tree | 3e05dce982c2bebb63f432064136d927a227e0c7 /plugins/xml | |
| parent | 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea (diff) | |
Nicer code concerning dirpaths and modpath around Lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
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 -> |