| Right _ -> "right"
| Ring _ -> "ring"
| Split _ -> "split"
+ | Subst _ -> "subst"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
(* Tattiche Aggiunte *)
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
| 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
| 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 _ -> ";"