]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
- Procedural: new flag "level=n" to control the reconstruction level (defaults to...
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index ce7fdcfdf07c120df09274a994cf17de7b82d1d8..6806713a4e9375a4c20ca4009d666c54d62720ea 100644 (file)
@@ -282,8 +282,9 @@ let pp_macro ~term_pp ~lazy_term_pp =
         | IPPrefix prefix -> "prefix = \"" ^ prefix ^ "\""
        | IPAs flavour -> flavour_pp flavour
        | IPProcedural -> "procedural"
-       | IPDepth depth -> "depth = " ^ string_of_int depth
        | IPNoDefaults -> "nodefaults"
+       | IPDepth depth -> "depth = " ^ string_of_int depth
+       | IPLevel level -> "level = " ^ string_of_int level
      in
      let s = String.concat " " (List.map pp_param l) in
      if s = "" then s else " " ^ s