aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml/xmlcommand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
-rw-r--r--contrib/xml/xmlcommand.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 6ac022c2d3..3d98375ddf 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -544,7 +544,7 @@ let show_pftreestate fn (kind,pftst) id =
let kn = Lib.make_kn id in
let env = Global.env () in
let obj = mk_current_proof_obj id val0 typ evar_map env in
- let uri = Cic2acic.uri_of_path (Lib.cwd()) id Cic2acic.Constant in
+ let uri = Cic2acic.uri_of_declaration id Cic2acic.Constant in
print_object_kind uri (kind_of_goal kind);
print_object uri obj evar_map
(Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr,