- performance data added for reference

[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 dc697bff424769f61b30522edbd1e13538fc0427..5dc3887c572799dd6b68c8722cadd41f79bf76b4 100644 (file)
--- a/helm/software/lambda-delta/basic_rg/brgOutput.ml
+++ b/helm/software/lambda-delta/basic_rg/brgOutput.ml
@@ -133,20 +133,17 @@ let print_counters f c =
 (* context/term pretty printing *********************************************)
 
 let id frm a =
-   let err () = assert false in
    let f n = function 
       | true  -> F.fprintf frm "%s" n
       | false -> F.fprintf frm "^%s" n
    in      
-   B.name err f a
+   B.name C.err f a
 
 let rec pp_term c frm = function
    | 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 
+      let err () = F.fprintf frm "@[*%u@]" h in
+      let f s = F.fprintf frm "@[%s@]" s in
+      H.get_sort err f h 
    | B.LRef (_, i)           -> 
       let err i = F.fprintf frm "@[#%u@]" i in
       let f _ a _ = F.fprintf frm "@[%a@]" id a in