]> matita.cs.unibo.it Git - helm.git/commitdiff
Tentative bug fix for diverging pretty-printing function.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Jul 2007 09:58:30 +0000 (09:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Jul 2007 09:58:30 +0000 (09:58 +0000)
helm/software/components/grafite/grafiteAstPp.ml

index 6dc488816f304193c834271b1273f51033f49e01..0b448659484067634158e73c91f023b0c6c02956 100644 (file)
@@ -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