Tentative bug fix for diverging pretty-printing function.

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 6dc488816f304193c834271b1273f51033f49e01..0b448659484067634158e73c91f023b0c6c02956 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/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