- we added a parser for lambda-delta textual syntax (file extension .hln)

[helm.git] / helm / software / lambda-delta / basic_rg / brgOutput.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml
index e4e7489ca3f3e2d864a399e1cc0f1e7d782ad471..124f9897402c3b01fce0e2ae4de51c2b1b6a814e 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -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