From: Claudio Sacerdoti Coen 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