]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgOutput.ml
improved type hierarchy management
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml
index 4d3eb0ff7f093d6dbd6bdba51ddbef183552c4a7..958408303f6e72af13e3aadcb6b43f75e7441ce0 100644 (file)
@@ -14,6 +14,7 @@ module F = Format
 module U = NUri
 module C = Cps
 module L = Log
+module H = Hierarchy
 module B = Brg
 
 type counters = {
@@ -98,7 +99,12 @@ let print_counters f c =
    f ()
 
 let rec pp_term c frm = function
-   | B.Sort h                 -> F.fprintf frm "@[*%u@]" h
+   | B.Sort h                 -> 
+      let f = function 
+         | Some s -> F.fprintf frm "@[%s@]" s
+        | None   -> F.fprintf frm "@[*%u@]" h
+      in
+      H.get_sort f h 
    | B.LRef i                 -> 
       let f = function
          | Some (id, _) -> F.fprintf frm "@[%s@]" id