we removed old HAL exportation (replaced by XML exportation)

[helm.git] / helm / software / lambda-delta / src / toplevel / metaOutput.ml

diff --git a/helm/software/lambda-delta/src/toplevel/metaOutput.ml b/helm/software/lambda-delta/src/toplevel/metaOutput.ml
index 859857ebe8c1a47efb1483bd948f0802149d09f6..2d9246f5dd407bb0c195c3506b82ceff9bad7a2a 100644 (file)
--- a/helm/software/lambda-delta/src/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/src/toplevel/metaOutput.ml
@@ -106,57 +106,3 @@ let print_counters f c =
    L.warn (P.sprintf "    Global Int. Complexity:   %7u" c.nodes);
    L.warn (P.sprintf "      + Abbreviation nodes:   %7u" nodes);
    f ()
-
-let string_of_sort = function
-   | true -> "Type"
-   | false -> "Prop"
-
-let pp_transparent frm a =
-   let err () = F.fprintf frm "%s" "=" in
-   let f () = F.fprintf frm "%s" "~" in
-   E.priv err f a
-
-let pp_list pp opend sep closed frm l =
-   let rec aux frm = function
-      | []       -> ()
-      | [hd]     -> pp frm hd
-      | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl 
-   in
-   if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
-
-let pp_rev_list pp opend sep closed frm l =
-   pp_list pp opend sep closed frm (List.rev l)
-
-let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
-
-and pp_term frm = function
-   | M.Sort s            -> 
-      F.fprintf frm "@[*%s@]" (string_of_sort s)
-   | M.LRef (l, i)       ->
-      F.fprintf frm "@[%u@@#%u@]" l i
-   | M.GRef (l, uri, ts) ->
-      F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts
-   | M.Appl (v, t)       ->
-      F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t
-   | M.Abst (id, w, t)   ->
-      F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
-
-let pp_par frm (id, w) =
-   F.fprintf frm "%s:%a" id pp_term w
-
-let pp_pars = pp_rev_list pp_par "[" "," "]"
-
-let pp_body a frm = function
-   | None   -> ()
-   | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t
-
-let pp_entity frm = function
-   | a, uri, E.Abst (pars, u, body)
-   | a, uri, E.Abbr (pars, u, body) ->
-      F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" 
-         (E.mark C.err C.start a) (U.string_of_uri uri) 
-        pp_pars pars (pp_body a) body pp_term u
-   | _, _, E.Void                   -> assert false
-
-let pp_entity f frm entity =
-   pp_entity frm entity; f ()