X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=0b448659484067634158e73c91f023b0c6c02956;hb=bb6a5a4cb3f8bc14764bb31eb46225004ad38cd0;hp=6dc488816f304193c834271b1273f51033f49e01;hpb=cb06122ec0250d63b18629e4a85f0515831114ce;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 6dc488816..0b4486594 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -75,11 +75,11 @@ let opt_string_pp = function
    | Some what -> what ^ " "
 
 let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
-  let pp_tactic = pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
-  let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
-  let pp_reduction_kind = pp_reduction_kind ~term_pp in
-  let pp_tactic_pattern =
-   pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
+ let pp_tactics = pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp in
+ let pp_reduction_kind = pp_reduction_kind ~term_pp in
+ let pp_tactic_pattern =
+  pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in
+ let rec pp_tactic =
   function
   (* Higher order tactics *)
   | Do (_, count, tac) ->
@@ -199,6 +199,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
        String.concat " "
         (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^  ")")
 	  args)
+ in pp_tactic
 
 and pp_tactics ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~sep tacs =
   String.concat sep