From bb6a5a4cb3f8bc14764bb31eb46225004ad38cd0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 20 Jul 2007 09:58:30 +0000 Subject: [PATCH] Tentative bug fix for diverging pretty-printing function. --- helm/software/components/grafite/grafiteAstPp.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) 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 -- 2.39.2