X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgOutput.ml;h=186349a1c6161d47a7c4817663c7124b3dcd6076;hb=6c4c95026020ae9924ac652482a8a0f731719e6c;hp=e4e7489ca3f3e2d864a399e1cc0f1e7d782ad471;hpb=3f6af93003bef461be59c8d4c96009c631f0c2e7;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgOutput.ml b/helm/software/lambda-delta/basic_rg/brgOutput.ml index e4e7489ca..186349a1c 100644 --- a/helm/software/lambda-delta/basic_rg/brgOutput.ml +++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml @@ -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 **************************************************************) @@ -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