Affichage des paths avec des '.', 2eme; prise en compte qualid

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@926 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 9 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index e17ca92f3..028fe1530 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -175,7 +175,7 @@ let pf_lookup_name_as_renamed hyps ccl s =
 let pf_lookup_index_as_renamed ccl n =
   Detyping.lookup_index_as_renamed ccl n
 
-let pr_idl idl = prlist_with_sep pr_spc print_id idl
+let pr_idl idl = prlist_with_sep pr_spc pr_id idl
 
 let pr_goal g =
   let env = evar_env g in
@@ -274,7 +274,7 @@ let pr_evd evd =
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pe = pr_decl evd in 
-       h 0 [< print_id (id_of_existential ev) ; 'sTR"==" ; pe >])
+       h 0 [< pr_id (id_of_existential ev) ; 'sTR"==" ; pe >])
     (Evd.to_list evd)
     
 let pr_decls decls = pr_evd (ts_it decls)
@@ -291,7 +291,7 @@ let pr_evars =
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pegl = pr_evgl_sign evd in 
-       [< print_id (id_of_existential ev); 'sTR " : "; pegl >])
+       [< pr_id (id_of_existential ev); 'sTR " : "; pegl >])
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
@@ -300,7 +300,7 @@ let rec pr_evars_int i = function
       let pegl = pr_evgl_sign evd in 
       let pei = pr_evars_int (i+1) rest in
       [< (hOV 0 [< 'sTR "Existential "; 'iNT i; 'sTR " ="; 'sPC;
-                   print_id (id_of_existential ev) ; 'sTR " : "; pegl >]); 
+                   pr_id (id_of_existential ev) ; 'sTR " : "; pegl >]); 
 	 'fNL ; pei >]
 
 let pr_subgoals_existential sigma = function 
@@ -349,10 +349,11 @@ let last_of_cvt_flags (_,red) =
   (if (red_set red BETA) then [ope("Beta",[])]
    else [])@
   (let (n_unf,lconst) = red_get_const red in
-   let lnvar = List.map (fun sp -> nvar (print_basename sp)) lconst in
-   if lnvar = [] then []
-   else if n_unf then [ope("Delta",[]);ope("UnfBut",lnvar)]
-   else [ope("Delta",[]);ope("Unf",lnvar)])@
+   let lqid = List.map (fun sp -> ast_of_qualid (Global.qualid_of_global 
+              (ConstRef sp))) lconst in
+   if lqid = [] then []
+   else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
+   else [ope("Delta",[]);ope("Unf",lqid)])@
   (if (red_set red IOTA) then [ope("Iota",[])]
    else [])
 
@@ -365,7 +366,8 @@ let ast_of_cvt_redexp = function
   | Lazy flg -> ope("Lazy",last_of_cvt_flags flg)
   | Unfold l ->
     ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
-      [nvar (print_basename sp)]@(List.map num locc))) l)
+      [ast_of_qualid (Global.qualid_of_global (ConstRef sp))]
+      @(List.map num locc))) l)
   | Fold l ->
     ope("Fold",List.map (fun c -> ope ("COMMAND",
       [ast_of_constr false (Global.env ()) c])) l)