]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagOutput.ml
- performance data added for reference
[helm.git] / helm / software / lambda-delta / basic_ag / bagOutput.ml
index 17bfe06596472933fb8a1522009d97fff2624a79..c315b1ec7a599052cfd877c7666d8cad09af8be0 100644 (file)
@@ -105,11 +105,9 @@ let res l id =
 
 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 f = function
          | Some (id, _) -> F.fprintf frm "@[%s@]" id