From a6d858b84132bcb27bcc771f06a854cc94eef716 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Oct 2001 12:49:19 +0000 Subject: Abstraction de l'immplementation de dirpath et implementation dans l'autre sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7 --- dev/top_printers.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index bc7a0b836f..cf35caf0cd 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -244,7 +244,7 @@ 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 ls = - match List.map string_of_id (dirpath sp) with + match List.map string_of_id (repr_dirpath (dirpath sp)) with ("Scratch"::l)-> l | ("Coq"::_::l) -> l | l -> l -- cgit v1.2.3