]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_rg/brgOutput.ml
txtLexer: bug fix in parsing the string tokens
[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml
index 70464fde7cbf5cf38ca0910ffcc1d99986d73ff4..186349a1c6161d47a7c4817663c7124b3dcd6076 100644 (file)
@@ -14,10 +14,10 @@ module F = Format
 module C = Cps
 module U = NUri
 module L = Log
+module O = Options
 module Y = Entity
 module X = Library
 module H = Hierarchy
-module O = Output
 module B = Brg
 
 (* nodes count **************************************************************)
@@ -135,7 +135,7 @@ let rename f e a =
    let rec aux f e n r =
       let f = function
          | true  -> f n r
-        | false -> aux f e (n ^ "'") r
+        | false -> aux f e (n ^ "_") r
       in
       does_not_occur f n r e
    in
@@ -158,7 +158,7 @@ let rec pp_term e frm = function
    | B.Sort (_, h)           -> 
       let err _ = F.fprintf frm "@[*%u@]" h in
       let f s = F.fprintf frm "@[%s@]" s in
-      H.get_sort err f h 
+      H.string_of_sort err f h 
    | B.LRef (_, i)           -> 
       let err _ = F.fprintf frm "@[#%u@]" i in
       if !O.indexes then err () else      
@@ -214,7 +214,7 @@ let rec exp_term e t out tab = match t with
       let a =
          let err _ = a in
          let f s = Y.Name (s, true) :: a in
-        H.get_sort err f l
+        H.string_of_sort err f l
       in
       let attrs = [X.position l; X.name a] in
       X.tag X.sort attrs out tab