Module Print

module Print: sig .. end
Pretty printing functions we use for the aac_instances tactic.

val print : Coq.Relation.t ->
Theory.Trans.ir ->
(int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m ->
Term.rel_context -> Proof_type.tactic
The main printing function. 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 Theory.Trans module.