From d7a64f8b6efd748625c8eb9aa2aef08ca618e5c6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Mar 2004 10:08:59 +0000
Subject: Fabrication de l'uri a partir du path utilisateur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5608 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'contrib/xml/xmlcommand.ml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 651b85b0cf..b120a95bc8 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_kernel_name kn Cic2acic.Constant in
+ let uri = Cic2acic.uri_of_path (Lib.cwd()) 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,
@@ -553,8 +553,7 @@ let show_pftreestate fn (kind,pftst) id =
 
 let show fn =
  let pftst = Pfedit.get_pftreestate () in
- let (_,kind,_,_) = Pfedit.current_proof_statement () in
- let id = Pfedit.get_current_proof_name () in
+ let (id,kind,_,_) = Pfedit.current_proof_statement () in
   show_pftreestate fn (kind,pftst) id
 ;;
 
-- 
cgit v1.2.3