sig
  val print :
    Coq.Relation.t ->
    Theory.Trans.ir ->
    (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
    EConstr.rel_context -> unit Proofview.tactic
end