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 ->
       EConstr.rel_context -> unit Proofview.tactic

The main printing function. Print.print uses the 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.