Bug fixed in pretty printing in new syntax of MutCases on inductive types

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 7d12c212947c4cc93702e8904962c8c88575989c..b78f6d90b5999c97646f88430f01d2f3be140c7f 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -152,6 +152,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Right _ -> "right"
   | Ring _ -> "ring"
   | Split _ -> "split"
+  | Subst _ -> "subst"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
   (* Tattiche Aggiunte *)
@@ -217,8 +218,8 @@ let pp_default what uris =
   sprintf "default \"%s\" %s" what
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
-let pp_coercion uri do_composites =
-   sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
+let pp_coercion uri do_composites arity =
+   sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
      (if do_composites then "compounds" else "no compounds")
     
 let pp_command ~obj_pp = function
@@ -227,7 +228,7 @@ let pp_command ~obj_pp = function
   | Drop _ -> "drop"
   | Print (_,s) -> "print " ^ s
   | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-  | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
+  | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
   | Obj (_,obj) -> obj_pp obj
   | Default (_,what,uris) ->
       pp_default what uris
@@ -247,6 +248,7 @@ let rec pp_tactical ~term_pp ~lazy_term_pp =
   | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
   | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
   | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
+  | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac
 
   | Dot _ -> "."
   | Semicolon _ -> ";"