From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 20 Jul 2007 09:58:30 +0000 (+0000)
Subject: Tentative bug fix for diverging pretty-printing function.
X-Git-Tag: 0.4.95@7852~299
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=361e74e8f714a12b22730fe3a303b12b10d4d7b6;p=helm.git

Tentative bug fix for diverging pretty-printing function.
---

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 6dc488816..0b4486594 100644
--- 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