- library/list/list.ma: unused code commented

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index cdf90c5b989883ff54a2e98d6a4c7e6c527901e8..26c73eb2fb3931b659de16e7e9398b4481f83811 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -282,13 +282,14 @@ let pp_macro ~term_pp ~lazy_term_pp =
      let pp_param = function
         | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
        | IPAs flavour  -> flavour_pp flavour
+       | IPCoercions   -> "coercions"
+       | IPDebug debug -> "debug = " ^ string_of_int debug
        | IPProcedural  -> "procedural"
        | IPNoDefaults  -> "nodefaults"
        | IPDepth depth -> "depth = " ^ string_of_int depth
        | IPLevel level -> "level = " ^ string_of_int level
        | IPComments    -> "comments"
-       | IPCoercions   -> "coercions"
-       | IPDebug debug -> "debug = " ^ string_of_int debug
+       | IPCR          -> "cr"
      in
      let s = String.concat " " (List.map pp_param l) in
      if s = "" then s else " " ^ s