From e5643982202eeddf2c4fb7808d5c530a87009e89 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Apr 2003 18:13:14 +0000
Subject: Globalisation tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3860 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/top_printers.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ac5e3d0c81..29cfe5c2a6 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -91,7 +91,7 @@ let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]")
 
 let ppenv e = pp (pr_rel_context e (rel_context e))
 
-let pptac = (fun x -> pp(Pptactic.pr_raw_tactic x))
+let pptac = (fun x -> pp(Pptactic.pr_glob_tactic x))
 
 let pr_obj obj = Format.print_string (Libobject.object_tag obj)
 
@@ -258,14 +258,14 @@ let print_pure_constr csr =
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
   and sp_display sp = 
-    let dir,l = decode_kn sp in
+(*    let dir,l = decode_kn sp in
     let ls = 
       match List.rev (List.map string_of_id (repr_dirpath dir)) with 
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l 
 	| l             -> l
-    in  List.iter (fun x -> print_string x; print_string ".") ls;
-      print_string (string_of_id l)
+    in  List.iter (fun x -> print_string x; print_string ".") ls;*)
+      print_string (string_of_kn sp)
 
   in
      box_display csr; print_flush()
-- 
cgit v1.2.3