X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=ae9aa50270319ef2cedf6eee81c6e995633f1ede;hb=d97f69b313893900ca2d57544fcd200eb06ee286;hp=84facde66203a3e9ac62ba4c1afe4c1b5120f3c0;hpb=ed5c4e15429c37bef0f59dfd7160f6883586ed0f;p=helm.git diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 84facde66..ae9aa5027 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -288,15 +288,15 @@ let pp_default what uris = Printf.sprintf "default \"%s\" %s" what (String.concat " " (List.map UriManager.string_of_uri uris)) -let pp_coercion uri do_composites arity saturations= +let pp_coercion ~term_pp t do_composites arity saturations= Printf.sprintf "coercion %s %d %d %s" - (UriManager.string_of_uri uri) arity saturations + (term_pp t) arity saturations (if do_composites then "" else "nocomposites") let pp_command ~term_pp ~obj_pp = function | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri - | Coercion (_, uri, do_composites, i, j) -> - pp_coercion uri do_composites i j + | Coercion (_, t, do_composites, i, j) -> + pp_coercion ~term_pp t do_composites i j | Default (_,what,uris) -> pp_default what uris | Drop _ -> "drop" | Include (_,path) -> "include \"" ^ path ^ "\""