module AAC_print:Pretty printing functions we use for the aac_instances tactic.sig
..end
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
AAC_print.print
uses the Term.rel_context
to rename the variables, and rebuilds raw Coq terms (for the given
context, and the terms in the environment). In order to do so, it
requires the information gathered by the AAC_theory.Trans
module.