sig
  val print :
    AAC_coq.Relation.t ->
    AAC_theory.Trans.ir ->
    (int * AAC_matcher.Terms.t * AAC_matcher.Subst.t AAC_search_monad.m)
    AAC_search_monad.m -> Term.rel_context -> Proof_type.tactic
end